mdh.sePublications
Change search
Link to record
Permanent link

Direct link
BETA
Publications (10 of 22) Show all publications
Kunnappilly, A., Marinescu, R. & Seceleanu, C. (2019). A Model-Checking-Based Framework For Analyzing Ambient Assisted Living Solutions. Sweden
Open this publication in new window or tab >>A Model-Checking-Based Framework For Analyzing Ambient Assisted Living Solutions
2019 (English)Report (Refereed)
Place, publisher, year, edition, pages
Sweden: , 2019
National Category
Embedded Systems
Identifiers
urn:nbn:se:mdh:diva-42920 (URN)
Note

Since modern ambient assisted living solutions integrate a multitude of assisted-living functionalities within a common design framework, some are safety-critical, it is desirable that these systems are analyzed already at their design stage to detect possible errors. To achieve this, one needs suitable architectures that support the seamless design of the integrated assisted-living functions, as well as capabilities for the formal modeling and analysis of the architecture. In this paper, we attempt to address this need, by proposing a generic integrated ambient assisted living system architecture, consisting of sensors, data-collector, local and cloud processing schemes, and an intelligent decision support system, which can be easily extended to suite specific architecture categories. Our solution is customizable, therefore, we show three instantiations of the generic model, as simple, intermediate and complex configuration, respectively, and show how to analyze the first and third categories by model checking. Our approach starts by specifying the architecture, using an architecture description language, in our case, the Architecture Analysis and Design Language that can also account for the probabilistic behavior of such systems. To enable formal analysis, we describe the semantics of the simple and complex categories as stochastic timed automata. The former we model check exhaustively with UPPAAL, whereas for the latter we employ statistical model checking using UPPAAL SMC, the statistical extension of UPPAAL, for scalability reasons.

Available from: 2019-03-14 Created: 2019-03-14 Last updated: 2019-06-11Bibliographically approved
Gu, R., Marinescu, R., Seceleanu, C. & Lundqvist, K. (2019). Towards a Two-layer Framework for Verifying Autonomous Vehicles. In: NASA Formal Methods. NFM 2019. Lecture Notes in Computer Science, vol 11460: . Paper presented at 11th Annual NASA Formal Methods Symposium NFM 2019, 07 May 2019, Houston, United States.
Open this publication in new window or tab >>Towards a Two-layer Framework for Verifying Autonomous Vehicles
2019 (English)In: NASA Formal Methods. NFM 2019. Lecture Notes in Computer Science, vol 11460, 2019Conference paper, Published paper (Refereed)
Abstract [en]

Autonomous vehicles rely heavily on intelligent algorithms for path planning and collision avoidance, and their functionality and dependability could be ensured through formal verification. To facilitate the verification, it is beneficial to decouple the static high-level planning from the dynamic functions like collision avoidance. In this paper, we propose a conceptual two-layer framework for verifying autonomous vehicles, which consists of a static layer and a dynamic layer. We focus concretely on modeling and verifying the dynamic layer using hybrid automata and UPPAAL SMC, where a continuous movement of the vehicle as well as collision avoidance via a dipole flow field algorithm are considered. This framework achieves decoupling by separating the verification of the vehicle's autonomous path planning from that of the vehicle autonomous operation in a continuous dynamic environment. To simplify the modeling process, we propose a pattern-based design method, where patterns are expressed as hybrid automata. We demonstrate the applicability of the dynamic layer of our framework on an industrial prototype of an autonomous wheel loader.

Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 11460
National Category
Engineering and Technology Computer Systems
Identifiers
urn:nbn:se:mdh:diva-43924 (URN)10.1007/978-3-030-20652-9_12 (DOI)2-s2.0-85066869584 (Scopus ID)9783030206512 (ISBN)
Conference
11th Annual NASA Formal Methods Symposium NFM 2019, 07 May 2019, Houston, United States
Projects
DPAC - Dependable Platforms for Autonomous systems and Control
Available from: 2019-06-19 Created: 2019-06-19 Last updated: 2019-06-20Bibliographically approved
Kunnappilly, A., Marinescu, R. & Seceleanu, C. (2018). Assuring intelligent ambient assisted living solutions by statistical model checking. In: Lect. Notes Comput. Sci.: . Paper presented at 5 November 2018 through 9 November 2018 (pp. 457-476). Springer Verlag
Open this publication in new window or tab >>Assuring intelligent ambient assisted living solutions by statistical model checking
2018 (English)In: Lect. Notes Comput. Sci., Springer Verlag , 2018, p. 457-476Conference paper, Published paper (Refereed)
Abstract [en]

A modern way of enhancing elderly people’s quality of life is by employing various Ambient Assisted Living solutions that facilitate an independent and safe living for their users. This is achieved by integrating computerized functions such as health and home monitoring, fall detection, reminders, etc. Such systems are safety critical, therefore ensuring at design time that they operate correctly, but also in a timely and robust manner is important. Most of the solutions are not analyzed formally at design time, especially if such Ambient Assisted Living functions are integrated within the same design. To address this concern, we propose a framework that relies on an abstract component-based description of the system’s architecture in the Architecture Analysis and Design Language. To ensure scalability of analysis, we transform the AADL models into a network of stochastic timed automata amenable to statistical analysis of various quality-of-service attributes. The architecture that we analyze is developed as part of the project CAMI, co-financed by the European Commission, and consists of a variety of health and home sensors, a data collector, local and cloud processing, as well as an artificial-intelligence-based decision support system. Our contribution paves the way towards achieving design-time assured integrated Ambient Assisted Living solutions, which in turn could reduce verification effort at later stages.

Place, publisher, year, edition, pages
Springer Verlag, 2018
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 11245 LNCS
Keywords
Artificial intelligence, Computer architecture, Decision support systems, Formal methods, Model checking, Network architecture, Quality control, Quality of service, Safety engineering, Stochastic models, Stochastic systems, Ambient assisted living, Architecture analysis, Cloud processing, Component based, Design languages, European Commission, Home monitoring, Statistical model checking, Assisted living
National Category
Computer and Information Sciences
Identifiers
urn:nbn:se:mdh:diva-41449 (URN)10.1007/978-3-030-03421-4_29 (DOI)2-s2.0-85056457127 (Scopus ID)9783030034207 (ISBN)
Conference
5 November 2018 through 9 November 2018
Available from: 2018-11-29 Created: 2018-11-29 Last updated: 2019-03-14Bibliographically approved
Gu, R., Marinescu, R., Seceleanu, C. & Lundqvist, K. (2018). Formal verification of an Autonomous Wheel Loader by model checking. In: Proceedings - International Conference on Software Engineering: . Paper presented at 6th ACM/IEEE Conference on Formal Methods in Software Engineering, FormaliSE 2018, co-located with International Conference on Software Engineering, ICSE 2018, 2 June 2018 (pp. 74-83). IEEE Computer Society
Open this publication in new window or tab >>Formal verification of an Autonomous Wheel Loader by model checking
2018 (English)In: Proceedings - International Conference on Software Engineering, IEEE Computer Society , 2018, p. 74-83Conference paper, Published paper (Refereed)
Abstract [en]

In an attempt to increase productivity and the workers' safety, the construction industry is moving towards autonomous construction sites, where various construction machines operate without human intervention. In order to perform their tasks autonomously, the machines are equipped with different features, such as position localization, human and obstacle detection, collision avoidance, etc. Such systems are safety critical, and should operate autonomously with very high dependability (e.g., by meeting task deadlines, avoiding (fatal) accidents at all costs, etc.). An Autonomous Wheel Loader is a machine that transports materials within the construction site without a human in the cab. To check the dependability of the loader, in this paper we provide a timed automata description of the vehicle's control system, including the abstracted path planning and collision avoidance algorithms used to navigate the loader, and we model check the encoding in UPPAAL, against various functional, timing and safety requirements. The complex nature of the navigation algorithms makes the loader's abstract modeling and the verification very challenging. Our work shows that exhaustive verification techniques can be applied early in the development of autonomous systems, to enable finding potential design errors that would incur increased costs if discovered later.

Place, publisher, year, edition, pages
IEEE Computer Society, 2018
Keywords
Autonomous Vehicle, Collision Avoidance, Formal Verification, Model Checking, Timed Automata, UPPAAL, Accident prevention, Automata theory, Construction equipment, Construction industry, Loaders, Mining machinery, Motion planning, Obstacle detectors, Wheels, Autonomous constructions, Autonomous Vehicles, Construction machines, Navigation algorithms, Safety requirements, Verification techniques
National Category
Electrical Engineering, Electronic Engineering, Information Engineering
Identifiers
urn:nbn:se:mdh:diva-40747 (URN)10.1145/3193992.3193999 (DOI)2-s2.0-85052130860 (Scopus ID)9781450357180 (ISBN)
Conference
6th ACM/IEEE Conference on Formal Methods in Software Engineering, FormaliSE 2018, co-located with International Conference on Software Engineering, ICSE 2018, 2 June 2018
Available from: 2018-09-07 Created: 2018-09-07 Last updated: 2018-09-07Bibliographically approved
Marinescu, R., Filipovikj, P., Enoiu, E. P., Larsson, J. & Seceleanu, C. (2017). An Energy-aware Mutation Testing Framework for EAST-ADL Architectural Models. In: 29th Nordic Workshop on Programming Theory NWPT'17: . Paper presented at 29th Nordic Workshop on Programming Theory NWPT'17, 01 Nov 2017, Turku, Finland , Finland (pp. 40-43). Turku, Finland , Finland: TUCS Lecture Notes
Open this publication in new window or tab >>An Energy-aware Mutation Testing Framework for EAST-ADL Architectural Models
Show others...
2017 (English)In: 29th Nordic Workshop on Programming Theory NWPT'17, Turku, Finland , Finland: TUCS Lecture Notes , 2017, p. 40-43Conference paper, Published paper (Refereed)
Abstract [en]

Early design artifacts of embedded systems, such as architectural models, represent convenient abstractions for reasoning about a system’s structure and functionality. One such example is the Electronic Architecture and Software Tools-Architecture Description Language (EAST-ADL), a domain-specific architectural language that targets the automotive industry. EAST-ADL is used to represent both hardware and software elements, as well as related extra-functional information (e.g., timing properties, triggering information, resource consumption). Testing architectural models is an important activity in engineering large-scale industrial systems, which sparks a growing research interest. Modern embedded systems, such as autonomous vehicles and robots, have low-energy computing demands, making testing for energy usage increasingly important. Nevertheless, testing resource-aware properties of architectural models has received less attention than the functional testing of such models. In our previous work, we have outlined a method for testing energy consumption in embedded systems using manually created faults based on statistical model checking of a priced formal system model. In this paper, we extend our previous work by showing how mutation testing] can be used to generate and select test cases based on the concept of energy-aware mutants– small syntactic modifications in the architectural model, intended to mimic real energy faults. Test cases that can distinguish a certain behavior from its mutations are sensitive to changes in the model, and hence considered to be good at detecting faults. The main contributions of this paper are: (i) an approach for creating energy-related mutants for EAST-ADL architectural models, (ii) a method for overcoming the equivalent mutant problem (i.e., the problem of finding a test case which can distinguish the observable behavior of a mutant from the original one), (iii) a test generation approach based on UPPAAL Statistical Model Checker (SMC), and (iv) a test selection criteria based on mutation analysis using our MATS tool.

Place, publisher, year, edition, pages
Turku, Finland , Finland: TUCS Lecture Notes, 2017
National Category
Computer Systems
Identifiers
urn:nbn:se:mdh:diva-37338 (URN)978-952-12-3608-2 (ISBN)
Conference
29th Nordic Workshop on Programming Theory NWPT'17, 01 Nov 2017, Turku, Finland , Finland
Projects
VeriSpec - Structured Specification and Automated Verification for Automotive Functional SafetyCAMI - Artificially intelligent ecosystem for self-management and sustainable quality of life in AAL (Ambient Assisted Living)DPAC - Dependable Platforms for Autonomous systems and ControlMegaMaRt2 - Megamodelling at Runtime (ECSEL/Vinnova)
Available from: 2017-11-28 Created: 2017-11-28 Last updated: 2018-10-31Bibliographically approved
Filipovikj, P., Mahmud, N., Marinescu, R., Rodriguez-Navas, G., Seceleanu, C., Ljungkrantz, O. & Lönn, H. (2017). Analyzing Industrial Simulink Models by Statistical Model Checking. Västerås, Sweden: Mälardalen Real-Time Research Centre, Mälardalen University
Open this publication in new window or tab >>Analyzing Industrial Simulink Models by Statistical Model Checking
Show others...
2017 (English)Report (Other academic)
Abstract [en]

The evolution of automotive systems has been rapid. Nowadays, electronic brains control dozens of functions in vehicles, like braking, cruising, etc. Model-based design approaches, in environments such as MATLAB Simulink, seem to help in addressing the ever-increasing need to enhance quality, and manage complexity, by supporting functional design from predefined block libraries, which can be simulated and analyzed for hidden errors, but also used for code generation. For this reason, providing assurance that Simulink models fulfill given functional and timing requirements is desirable. In this paper, we propose a pattern-based, execution-order preserving automatic transformation of Simulink atomic and composite blocks into stochastic timed automata that can then be analyzed formally with UPPAAL Statistical Model Checker (UPPPAAL SMC). Our method is supported by the tool SIMPPAAL, which we also introduce and apply on an industrial prototype called the Brake-by-Wire system. This work enables the formal analysis of industrial Simulink models, by automatically generating their semantic counterpart.

Place, publisher, year, edition, pages
Västerås, Sweden: Mälardalen Real-Time Research Centre, Mälardalen University, 2017
Series
MRTC Reports, ISSN 1404-3041
National Category
Engineering and Technology Computer Systems
Identifiers
urn:nbn:se:mdh:diva-35069 (URN)MDH-MRTC-316/2017-1-SE (ISRN)
Projects
VeriSpec - Structured Specification and Automated Verification for Automotive Functional Safety
Available from: 2017-03-27 Created: 2017-03-27 Last updated: 2019-05-08Bibliographically approved
Marinescu, R., Enoiu, E. P., Seceleanu, C. & Sundmark, D. (2017). Automatic Test Generation for Energy Consumption of Embedded Systems Modeled in EAST-ADL. In: Proceedings - 10th IEEE International Conference on Software Testing, Verification and Validation Workshops, ICSTW 2017: . Paper presented at 10th IEEE International Conference on Software Testing, Verification and Validation Workshops, ICSTW 2017, 13 March 2017 through 17 March 2017 (pp. 69-76).
Open this publication in new window or tab >>Automatic Test Generation for Energy Consumption of Embedded Systems Modeled in EAST-ADL
2017 (English)In: Proceedings - 10th IEEE International Conference on Software Testing, Verification and Validation Workshops, ICSTW 2017, 2017, p. 69-76Conference paper, Published paper (Refereed)
Abstract [en]

Testing using architectural design models is intended to determine if the realized system meets its specification, and works as a whole in terms of computational components and their interactions. The growing complexity of embedded systems requires new techniques that are able to support testing of extra-functional requirements, like energy usage of components and systems, which is very necessary in order to obtain valid implementations. In this paper, we show how architectural models described in the EAST-ADL architectural language can also be used for testing the energy consumption of embedded systems, after transforming them into networks of formal models called priced timed automata. Assuming an EAST-ADL model annotated with energy consumption information, we show how to automatically generate energy-aware test cases based on statistical model checking (SMC) of the resulting network of priced timed automata. We automate the generation of executable test cases with UPPAAL SMC, using a test strategy based on several random simulation runs of the system. By seeding the original formal model with a set of energy-consumption related faults, we are able to carry out fault detection analysis. We apply this technique on a Brake-by-Wire system from the automotive domain, and evaluate it in terms of efficiency and model fault detection. 

Series
IEEE International Conference on Software Testing Verification and Validation Workshops, ISSN 2159-4848
National Category
Computer Systems
Identifiers
urn:nbn:se:mdh:diva-35337 (URN)10.1109/ICSTW.2017.19 (DOI)000403392800013 ()2-s2.0-85018418022 (Scopus ID)9781509066766 (ISBN)
Conference
10th IEEE International Conference on Software Testing, Verification and Validation Workshops, ICSTW 2017, 13 March 2017 through 17 March 2017
Available from: 2017-05-19 Created: 2017-05-19 Last updated: 2018-10-31Bibliographically approved
Marinescu, R. (2016). Model-driven Analysis and Verification of Automotive Embedded Systems. (Doctoral dissertation). Västerås: Mälardalen University
Open this publication in new window or tab >>Model-driven Analysis and Verification of Automotive Embedded Systems
2016 (English)Doctoral thesis, comprehensive summary (Other academic)
Abstract [en]

Modern vehicles are equipped with electrical and electronic systems that implement highly complex functions, such as anti-lock braking, cruise control, etc. To realize and integrate such complex embedded systems, the automotive development process requires an updated methodology that takes into consideration the system’s intricate features and examines both their functional and extra-functional requirements. Early design artifacts like architectural models represent convenient abstractions for reasoning about the system’s structure and functionality. In this context, the EAST-ADL language has been developed as a domain-specific architectural language that targets the automotive industry and is aligned with the AUTOSAR automotive standard. To fully enjoy the benefits of these abstract system descriptions, architectural models need to be integrated into a model-driven development framework that enables also verification by, e.g., model checking and model-based testing. One major drawback in developing such a framework lies in the fact that architectural models, while capturing the system’s structure and inter-component communication, often lack direct means to represent the desired internal behavior of the system in a semantically well-defined way. To overcome this, one needs to provide means of integrating both structural as well as behavioral information, desirably within the same framework backed by formal semantics, in order to enable the model’s formal verification.

In this thesis, we propose a tool-supported integrated formal modeling and verification framework tailored for automotive embedded systems that are originally described in the EAST-ADL architectural language. To achieve this, we first provide formal semantics to the architectural model and its behavior by proposing an equivalent formal description as a network of timed automata. This enables us to analyze the resulting network of timed automata formally by model checking, using both the UPPAAL PORT and UPPAAL SMC model checkers. UPPAAL PORT is providing efficient component-aware verification via the partial order reduction technique, while UPPAAL SMC is extending UPPAAL with statistical model-checking capabilities via probabilistic algorithms. We focus the analysis on functional and timing requirements, but also on the system’s resource usage with respect to different resources specified in the model, such as memory and energy. In an attempt to narrow the gap between the original architectural model and the eventual system implementation, we define an executable semantics of the UPPAAL PORT components that guarantees that the implementation preserves the invariant properties of the model. Assuming a system implementation that conforms to the formal model, we investigate how to provide test cases suitable for the eventual verification of such implementation, by exploiting the model checker’s ability to generate witness traces for reachability verification. Such a witness trace represents a execution of the system from its initial state to the goal state encoded by the reachability property, and becomes our abstract test case. By pairing the automated model-based test case generator with an automatic transformation from the abstract test cases to Python scripts, we enable the execution of the generated Python scripts on the system under test, which ends up in pass/fail testing verdicts. Dependency analysis is a method that is able to identify crucial intra- and inter-component dependencies early in the system’s development life cycle, if applied on architectural models. In this thesis, we also investigate how such dependencies, resulting from applying dependency analysis on EAST-ADL models, can be exploited during formal verification in order to reduce the verified state-spaces during model checking. The framework is supported by the ViTAL tool and its applicability is shown on an automotive industrial prototype, namely a Brake-by-Wire system. 

Place, publisher, year, edition, pages
Västerås: Mälardalen University, 2016
Series
Mälardalen University Press Dissertations, ISSN 1651-4238 ; 206
National Category
Embedded Systems
Research subject
Computer Science
Identifiers
urn:nbn:se:mdh:diva-32463 (URN)978-91-7485-278-3 (ISBN)
External cooperation:
Public defence
2016-10-07, Gamma, Mälardalens högskola, Västerås, 13:15 (English)
Opponent
Supervisors
Available from: 2016-08-17 Created: 2016-08-17 Last updated: 2016-09-12Bibliographically approved
Marinescu, R., Mubeen, S. & Seceleanu, C. (2016). Pruning Architectural Models of Automotive Embedded Systems via Dependency Analysis. In: 42nd Euromicro Conference series on Software Engineering and Advanced Applications SEAA 2016: . Paper presented at 42nd Euromicro Conference series on Software Engineering and Advanced Applications SEAA 2016, 31 Aug 2016, Cyprus, Cyprus (pp. 293-302).
Open this publication in new window or tab >>Pruning Architectural Models of Automotive Embedded Systems via Dependency Analysis
2016 (English)In: 42nd Euromicro Conference series on Software Engineering and Advanced Applications SEAA 2016, 2016, p. 293-302Conference paper, Published paper (Refereed)
National Category
Electrical Engineering, Electronic Engineering, Information Engineering
Identifiers
urn:nbn:se:mdh:diva-33749 (URN)10.1109/SEAA.2016.47 (DOI)000386649000043 ()2-s2.0-85020720799 (Scopus ID)978-1-5090-2819-1 (ISBN)
Conference
42nd Euromicro Conference series on Software Engineering and Advanced Applications SEAA 2016, 31 Aug 2016, Cyprus, Cyprus
Projects
PRESS - Predictable Embedded Software SystemsCAMI - Artificially intelligent ecosystem for self-management and sustainable quality of life in AAL (Ambient Assisted Living)
Available from: 2016-11-21 Created: 2016-11-21 Last updated: 2017-06-29Bibliographically approved
Marinescu, R., Seceleanu, C., Le Guen, H. & Pettersson, P. (2015). A Research Overview of Tool-Supported Model-based Testing of Requirements-based Designs. In: Advances in Computers: (pp. 89-140). Cornelsen, 98
Open this publication in new window or tab >>A Research Overview of Tool-Supported Model-based Testing of Requirements-based Designs
2015 (English)In: Advances in Computers, Cornelsen, 2015, Vol. 98, p. 89-140Chapter in book (Refereed)
Abstract [en]

Software testing aims at gaining confidence in software products through fault detection, by observing the differences between the behavior of the implementation and the expected behavior described in the specification. Nowadays, testing is the main verification technique used in industry, being a time and resource consuming activity. This has boosted the development of potentially more efficient testing techniques, like model-based testing, where test creation and execution can be automated, using an abstract system model as input. In this chapter, we provide an overview of the state-of-the-art in tool-supported model-based testing that starts from requirements-based models, by presenting and classifying some of the most mature tools available at this moment. Our goal is to get a deeper insight into the state-of-the-art in this area, as well as to form a position with respect to possible needs and gaps in the current tools used by industry and academia, which need to be addressed in order to enhance the applicability of model-based testing techniques. To achieve this, we extend an existing taxonomy with: (i) the test artifact, representing the type of information encoded in the model for the purpose of testing (i.e., functional behavior, extra-functional behavior, or the architectural description), and (ii) the mapping of test cases, which describes ways of using the generated test cases on the actual system under test. To provide further evidence of the inner-workings of different model-based testing tools, we select four representative tools (i.e, ProTest, UPPAAL Cover, MaTeLo, and CompleteTest) that we apply on a simple yet illustrative Coffee/Tea Vending Machine example, to show the differences in modeling notations, test case generation methods, and the produced test-cases. 

Place, publisher, year, edition, pages
Cornelsen, 2015
Keywords
Classification, Formal modeling, Literature review, Model-based testing, Model-checking, Requirements-based design, Survey, Taxonomy, Tool support, Tools for model-based testing
National Category
Computer Systems
Identifiers
urn:nbn:se:mdh:diva-29464 (URN)10.1016/bs.adcom.2015.03.003 (DOI)000370521900004 ()2-s2.0-84945485590 (Scopus ID)9780128021323 (ISBN)
Available from: 2015-11-12 Created: 2015-11-12 Last updated: 2016-12-27Bibliographically approved
Organisations
Identifiers
ORCID iD: ORCID iD iconorcid.org/0000-0002-7663-5497

Search in DiVA

Show all publications