mdh.sePublications
Change search
Refine search result
1 - 24 of 24
CiteExportLink to result list
Permanent link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Rows per page
  • 5
  • 10
  • 20
  • 50
  • 100
  • 250
Sort
  • Standard (Relevance)
  • Author A-Ö
  • Author Ö-A
  • Title A-Ö
  • Title Ö-A
  • Publication type A-Ö
  • Publication type Ö-A
  • Issued (Oldest first)
  • Issued (Newest first)
  • Created (Oldest first)
  • Created (Newest first)
  • Last updated (Oldest first)
  • Last updated (Newest first)
  • Disputation date (earliest first)
  • Disputation date (latest first)
  • Standard (Relevance)
  • Author A-Ö
  • Author Ö-A
  • Title A-Ö
  • Title Ö-A
  • Publication type A-Ö
  • Publication type Ö-A
  • Issued (Oldest first)
  • Issued (Newest first)
  • Created (Oldest first)
  • Created (Newest first)
  • Last updated (Oldest first)
  • Last updated (Newest first)
  • Disputation date (earliest first)
  • Disputation date (latest first)
Select
The maximal number of hits you can export is 250. When you want to export more records please use the Create feeds function.
  • 1.
    Enoiu, Eduard Paul
    et al.
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Marinescu, Raluca
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Causevic, Aida
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Seceleanu, Cristina
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    A Design Tool for Service-oriented Systems2013In: Electronical Notes in Theoretical Computer Science, ISSN 1571-0661, E-ISSN 1571-0661, Vol. 295, p. 95-100Article in journal (Other academic)
    Abstract [en]

    In this paper we present a modeling and analysis tool for service-oriented systems. The tool enables graphical modeling of service-based systems, within the resource-aware timed behavioral language Remes, as well as a textual system description. We have developed a graphical environment where services can be composed as desired by the user, together with a textual service composition interface in which compositions can also be checked for correctness. We also provide automated traceability between the two design interfaces, which results in a tool that enhances the potential of system design by intuitive service manipulation. The paper presents the design principles, infrastructure, and the user interface of our tool.

  • 2.
    Enoiu, Eduard Paul
    et al.
    Mälardalen University.
    Marinescu, Raluca
    Mälardalen University, School of Innovation, Design and Engineering.
    Seceleanu, Cristina
    Mälardalen University, School of Innovation, Design and Engineering.
    Paul, Pettersson
    Mälardalen University, School of Innovation, Design and Engineering.
    ViTAL : A Verification Tool for EAST-ADL Models using UPPAAL PORT2012In: Proceedings of the 17th IEEE International Conference on Engineering of Complex Computer Systems, Paris, France, 2012, p. 328-337Conference paper (Refereed)
    Abstract [en]

    A system’s architecture influence on the functions and other properties of embedded systems makes its high level analysis and verification very desirable. EAST-ADL is an architecture description language dedicated to automotive embedded system design with focus on structural and functional modeling. The behavioral description is not integrated within the execution semantics, which makes it harder to transform, analyze, and verify EAST-ADL models. Model-based techniques help address this issue by enabling automated transformation between different design models, and providing means for simulation and verification. We present a verification tool, called ViTAL, which provides the possibility to express the functional EAST-ADL behavior as timed automata models, which have precise semantics and can be formally verified. The ViTAL tool enables the transformation of EAST-ADL functional models to the UPPAAL PORT tool for model checking. This method improves the verification of functional and timing requirements in EAST-ADL, and makes it possible to identify dependencies and potential conflicts between different vehicle functions before the actual AUTOSAR implementation.

  • 3.
    Enoiu, Eduard Paul
    et al.
    Mälardalen University, School of Innovation, Design and Engineering.
    Marinescu, Raluca
    Mälardalen University, School of Innovation, Design and Engineering.
    Seceleanu, Cristina
    Mälardalen University, School of Innovation, Design and Engineering.
    Pettersson, Paul
    Mälardalen University, School of Innovation, Design and Engineering.
    Towards the Analysis and Verification of EAST-ADL Models using UPPAAL PORT2012Report (Other academic)
    Abstract [en]

    A system’s architecture influence on the functions and other properties of embedded systems makes its high level analysis and verification very desirable. EAST-ADL is an architecture description language dedicated to automotive embedded system design with focus on structural and functional modeling. The behavioral description is not integrated within the execution semantics, which makes it harder to transform, analyze, and verify EAST-ADL models. Model-based techniques help address this issue by enabling automated transformation between different design models, and providing means for simulation and verification. We present a verification tool, called ViTAL, which provides the possibility to express the functional EAST-ADL behavior as timed automata models, which have precise semantics and can be formally verified. The ViTAL tool enables the transformation of EAST-ADL functional models to the UPPAAL PORT tool for model checking. This method improves the verification of functional and timing requirements in EAST-ADL, and makes it possible to identify dependencies and potential conflicts between different vehicle functions before the actual AUTOSAR implementation.

  • 4.
    Filipovikj, Predrag
    et al.
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Mahmud, Nesredin
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Marinescu, Raluca
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Rodriguez-Navas, Guillermo
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Seceleanu, Cristina
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Ljungkrantz, Oscar
    Volvo Group Trucks Technology, Gothenburg, Sweden.
    Lönn, Henrik
    Volvo Group Trucks Technology, Gothenburg, Sweden.
    Analyzing Industrial Simulink Models by Statistical Model Checking2017Report (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.

  • 5.
    Filipovikj, Predrag
    et al.
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Mahmud, Nesredin
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Marinescu, Raluca
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Seceleanu, Cristina
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Ljungkrantz, Oscar
    Volvo Group Trucks TechnologyGothenburgSweden.
    Lönn, Henrik
    Volvo Group Trucks TechnologyGothenburgSweden.
    Simulink to UPPAAL Statistical Model Checker: Analyzing Automotive Industrial Systems2016In: FM 2016: Formal Methods, 2016, p. 748-756Conference paper (Refereed)
    Abstract [en]

    The advanced technology used for developing modern automotive systems increases their complexity, making their correctness assurance very tedious. To enable analysis, but also enhance understanding and communication, by simulation, engineers use MATLAB/Simulink modeling during system development. In this paper, we provide further analysis means to industrial Simulink models by proposing a pattern-based, execution-order preserving transformation of Simulink blocks into the input language of UPPAAL Statistical Model checker, that is, timed (hybrid) automata with stochastic semantics. The approach leads to being able to analyze complex Simulink models of automotive systems, and we report our experience with two vehicular systems, the Brake-by-Wire and the Adjustable Speed Limiter.

  • 6.
    Gu, Rong
    et al.
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Marinescu, Raluca
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Seceleanu, Cristina
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Lundqvist, Kristina
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Formal verification of an Autonomous Wheel Loader by model checking2018In: Proceedings - International Conference on Software Engineering, IEEE Computer Society , 2018, p. 74-83Conference 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.

  • 7.
    Gu, Rong
    et al.
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Marinescu, Raluca
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Seceleanu, Cristina
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Lundqvist, Kristina
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Towards a Two-layer Framework for Verifying Autonomous Vehicles2019In: NASA Formal Methods. NFM 2019. Lecture Notes in Computer Science, vol 11460, 2019Conference 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.

  • 8.
    Kang, Eun-Young
    et al.
    University of Namur, Belgium .
    Enoiu, Eduard Paul
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Marinescu, Raluca
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Seceleanu, Cristina
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Schnobbens, Pierre Yves
    University of Namur, Belgium .
    Pettersson, Paul
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    A Methodology for Formal Analysis and Verification of EAST-ADL Models2013In: Reliability Engineering & System Safety, ISSN 0951-8320, E-ISSN 1879-0836, Vol. 120, no Special Issue, p. 127-138Article in journal (Refereed)
    Abstract [en]

    The architectural design of embedded software has a direct impact on the final implementation, with respect to performance and other quality attributes. Therefore, guaranteeing that an architectural model meets the specified requirements is beneficial for detecting software flaws early in the development process. In this paper, we present a formal modeling and verification methodology for safety-critical automotive products that are originally described in the domain-specific architectural language East-adl. We propose a model-based approach that integrates the architectural models with component-aware model checking, and describe its tool support called ViTAL. The functional and timing behavior of each function block in the East-adl model, as well as the interactions between function blocks are formally captured and expressed as Timed Automata models, which have precise semantics and can be formally verified with ViTAL. Furthermore, we show how our approach, supported by ViTAL, can be used to formally prove that the East-adl system model fulfills the specified real-time requirements and behavioral constraints. We demonstrate that the approach improves the modeling and verification capability of East-adl and identifies dependencies, as well as potential conflicts between different automotive functions before implementation. The method is substantiated by verifying an automotive braking system model, with respect to particular functional and timing requirements.

  • 9.
    Kunnappilly, Ashalatha
    et al.
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Cai, Simin
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Marinescu, Raluca
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Seceleanu, Cristina
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Architecture Modelling and Formal Analysis of Intelligent Multi-Agent Systems2019In: Proceedings of the 14th International Conference on Evaluation of Novel Approaches to Software Engineering - Volume 1: ENASE, 2019, p. 114-126Conference paper (Refereed)
    Abstract [en]

    Modern cyber-physical systems usually assume a certain degree of autonomy. Such systems, like Ambient Assisted Living systems aimed at assisting elderly people in their daily life, often need to perform safety-critical functions, for instance, fall detection, health deviation monitoring, communication to caregivers, etc. In many cases, the system users have distributed locations, as well as different needs that need to be serviced intelligently at the same time. These features call for intelligent, adaptive, scalable and fault-tolerant system design solutions, which are well embodied by multi-agent architectures. Analyzing such complex architectures at design phase, to verify if an abstraction of the system satisfies all the critical requirements is beneficial. In this paper, we start from an agent-based architecture for ambient assisted living systems, inspired from the literature, which we model in the popular Architecture Description and Design Language. Since the latter lacks the ability to specify autonomous agent behaviours, which are often intelligent, non-deterministic or probabilistic, we extend the architectural language with a sub-language called Agent Annex, which we formally encode as a Stochastic Transition System. This contribution allows us to specify behaviours of agents involved in agent-based architectures of cyber-physical systems, which we show how to exhaustively verify with the state-of-art model checker PRISM. As a final step, we apply our framework on a distributed ambient assisted living system, whose critical requirements we verify with PRISM.

  • 10.
    Kunnappilly, Ashalatha
    et al.
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Marinescu, Raluca
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Seceleanu, Cristina
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    A Model-Checking-Based Framework For Analyzing Ambient Assisted Living Solutions2019Report (Refereed)
  • 11.
    Kunnappilly, Ashalatha
    et al.
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Marinescu, Raluca
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Seceleanu, Cristina
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Assuring intelligent ambient assisted living solutions by statistical model checking2018In: Lect. Notes Comput. Sci., Springer Verlag , 2018, p. 457-476Conference 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.

  • 12.
    Marinescu, Raluca
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Model-checking and Model-based Testing of Automotive Embedded Systems: Starting from the System Architecture2014Licentiate thesis, comprehensive summary (Other academic)
    Abstract [en]

    Nowadays, modern vehicles are equipped with electrical and electronic systems that implement highly complex functions such as anti-lock braking or cruise control. The use of such embedded systems in the automotive domain requires a revised development process that addresses their particular features. In this context, architectural models have been introduced in system development as convenient abstractions of the system’s structure represented as interacting components. To enjoy the full benefits of such abstractions, the architectural models should be complemented by an analysis framework that provides means for formal verification, and ideally also model-based testing, tailored to complex automotive systems. One major difficulty in developing such a framework lies in the fact that architectural models represent the system’s structure as well as inter-component communication, often without the actual description of the behavior. This entails the need to integrate the two “views” (structural and behavioral) in order to integrate them in a formal framework for verification.

    In this thesis, we propose an integrated formal modeling and analysis methodology for automotive embedded systems that are originally described in the domain-specific architectural language EAST-ADL. Our analysis methodology relies on formal veri- fication of the original EAST-ADL model by model-checking with UPPAAL PORT for component-based analysis, and UPPAAL SMC for statistical model-checking. To enable this, we first propose a formal description of the EAST-ADL components as networks of timed automata (TA), which are UPPAAL’s modeling language. Since C code implementation is in fact what is deployed on the vehicle, it is highly desirable to narrow the gap between the code and the architectural model, but also to test the implementation for various requirements. To accomplish the former, we define an exe- cutable semantics of the UPPAAL PORT components. To be able to support testing of EAST-ADL based implementations, we take advantage of the model-checker’s ability to generate witness traces during verification of reachability properties. Consequently, we employ UPPAAL PORT to generate such traces that become our abstract test-cases. 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 (our concrete test cases) on the system under test. The entire formal analysis and model-based testing framework is one solution to analyzing EAST-ADL models by model-checking techniques We show the framework’s applicability on an automotive industrial prototype, namely a Brake-by-Wire system. 

  • 13.
    Marinescu, Raluca
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Model-driven Analysis and Verification of Automotive Embedded Systems2016Doctoral 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. 

  • 14.
    Marinescu, Raluca
    et al.
    Mälardalen University, School of Innovation, Design and Engineering.
    Enoiu, Eduard Paul
    Mälardalen University, School of Innovation, Design and Engineering.
    Extending EAST-ADL for modeling and analysis of system's resource-usage2012In: Proceedings - International Computer Software and Applications Conference, 2012, p. 532-537Conference paper (Refereed)
    Abstract [en]

    EAST-ADL is an architectural description language dedicated to automotive embedded systems design, with focus on structural and functional modeling. The current architectural notations lack support for modeling and analysis of resource-usage, and therefore it is not possible to reason about resource requirements. In this paper, we describe our work towards filling the gap between EAST-ADL language and formal modeling and analysis of system’s resource usage, by extending the EAST-ADL language with embedded resources, such as storage, energy, communication and computation. To formalize this approach and provide a basis for rigorous analysis, we show how to analyze EAST-ADL models using the framework of priced timed automata and weighted CTL. We report our experiences from applying this approach for integrating resource-wise analysis into EAST-ADL.

  • 15.
    Marinescu, Raluca
    et al.
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Enoiu, Eduard Paul
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Seceleanu, Cristina
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Statistical Analysis of Resource Usage of Embedded Systems Modeled in EAST-ADL2015In: IEEE Computer Society Annual Symposium on VLSI (ISVLSI), 2015, p. 380-385Conference paper (Refereed)
    Abstract [en]

    The growing complexity of modern automotive embedded systems requires new techniques for model-based design that takes under consideration both software and hardware constraints and enables verification at early stages of development. In this context, EAST-ADL was developed as a domain specific language dedicated to modeling of functional-, software-, and hardware- architecture of automotive embedded systems. This language represents a convenient abstraction when reasoning about the system functionality and supports modeling of relevant extra-functional properties, like timing and resource usage. By providing formal semantics to the EAST-ADL language, as a network of priced timed automata, it becomes possible to reason about feasibility and worst-case resource consumption of the embedded components. In this paper, we show how to analyze such embedded systems modeled in EAST-ADL by using statistical model-checking. We report our experiences from applying this approach to an industrial Brake-by-Wire system.

  • 16.
    Marinescu, Raluca
    et al.
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Enoiu, Eduard Paul
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Seceleanu, Cristina
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Sundmark, Daniel
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Automatic Test Generation for Energy Consumption of Embedded Systems Modeled in EAST-ADL2017In: Proceedings - 10th IEEE International Conference on Software Testing, Verification and Validation Workshops, ICSTW 2017, 2017, p. 69-76Conference 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. 

  • 17.
    Marinescu, Raluca
    et al.
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Filipovikj, Predrag
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Enoiu, Eduard Paul
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Larsson, Jonatan
    Mälardalen University.
    Seceleanu, Cristina
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    An Energy-aware Mutation Testing Framework for EAST-ADL Architectural Models2017In: 29th Nordic Workshop on Programming Theory NWPT'17, Turku, Finland , Finland: TUCS Lecture Notes , 2017, p. 40-43Conference 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.

  • 18.
    Marinescu, Raluca
    et al.
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Kaijser, Henrik
    Volvo Group Trucks Technology, Gothenburg, Sweden .
    Mikuèionis, Marius
    Aalborg University, Denmark.
    Seceleanu, Cristina
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Lönn, Henrik
    Volvo Group Trucks Technology, Gothenburg, Sweden .
    David, Alexandre
    Aalborg University, Denmark.
    Analyzing Industrial Architectural Models by Simulation and Model-Checking2015In: Communications in Computer and Information Science, vol. 476, 2015, 2015, p. 189-205Conference paper (Refereed)
    Abstract [en]

    The software architecture of any automotive system has to be decided well in advance of production, so it is very desirable to assess its quality in order to obtain quick indications of errors at early design phases. In this paper, we present a constellation of analysis techniques for architectural models described in EAST-ADL. The methods are complementary in terms of covering EAST-ADL model analysis against a rich set of requirements, and in terms of the varying degree of confidence in the provided guarantees. Based on the needs of the current model- driven development in a chosen automotive context, we propose three analysis techniques of EAST-ADL architectural models, in an attempt to tackle some of the exposed design needs: simulation of EAST-ADL functions in Simulink, model-checking EAST-ADL models with timed automata semantics, and statistical model-checking in UPPAAL, applied on an automatically generated network of timed automata. An indus- trial Brake-by-Wire prototype is the case study on which we show the potential of simulating EAST-ADL models in Simulink, model-checking downscale EAST-ADL models, as well statistical model-checking of full model versions, in order to tame verification scalability problems.

  • 19.
    Marinescu, Raluca
    et al.
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Mubeen, Saad
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Seceleanu, Cristina
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Pruning Architectural Models of Automotive Embedded Systems via Dependency Analysis2016In: 42nd Euromicro Conference series on Software Engineering and Advanced Applications SEAA 2016, 2016, p. 293-302Conference paper (Refereed)
  • 20.
    Marinescu, Raluca
    et al.
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Saadatmand, Mehrdad
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Bucaioni, Alessio
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Seceleanu, Cristina
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Pettersson, Paul
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    A Model-Based Testing Framework for Automotive Embedded Systems2014In: The 40th Euromicro Conference on Software Engineering and Advanced Applications SEAA 2014, Verona, Italy, 2014Conference paper (Refereed)
    Abstract [en]

    Architectural models, such as those described in the EAST-ADL language, represent convenient abstractions to reason about automotive embedded software systems. To enjoy the fully-fledged advantages of reasoning, EAST-ADL models could benefit from a component-aware analysis framework that provides, ideally, both verification and model-based test-case generation capabilities. While different verification techniques have been developed for architectural models, only a few target EAST-ADL. In this paper, we present a methodology for code validation, starting from EAST-ADL artifacts. The methodology relies on: (i) automated model-based test-case generation for functional requirements criteria based on the EAST-ADL model extended with timed automata semantics, and (ii) validation of system implementation by generating Python test scripts based on the abstract test-cases, which represent concrete test-cases that are executable on the system implementation. We apply our methodology to analyze the ABS function implementation of a Brake-by-Wire system prototype.

  • 21.
    Marinescu, Raluca
    et al.
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Saadatmand, Mehrdad
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Bucaioni, Alessio
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Seceleanu, Cristina
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Pettersson, Paul
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    EAST-ADL Tailored Testing: From System Models to Executable Test Cases2013Report (Other academic)
    Abstract [en]

    Architectural models, such as those described in the EAST-ADL language, represent convenient abstractions to reason about embedded software systems. To enjoy the fully-fledged advantages of reasoning, EAST-ADL models require a component-aware analysis framework that provide, ideally, both verification and model-based test-case generation capabilities. In this paper, we extend ViTAL, our recently developed tool-supported framework for model-checking EAST-ADL models in Uppaal Port, with automated model-based test-case generation for functional requirements criteria. To validate the actual system implementation and exercise the feasibility of the abstract test-cases, we also show how to generate Python test scripts, from the ViTAL generated abstract test-cases. The scripts define the concrete test-cases that are executable on the system implementation, within the Farkle testing environment. Tool interoperability between ViTAL and Farkle is ensured by implementing a corresponding interface, compliant with the Open Services for Lifecycle collaboration (OSLC) standard. We apply our methodology to validate the ABS function implementation of a Brake-by-Wire system prototype.

  • 22.
    Marinescu, Raluca
    et al.
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Seceleanu, Cristina
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Le Guen, H.
    ALL4TEC, Laval, France.
    Pettersson, Paul
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    A Research Overview of Tool-Supported Model-based Testing of Requirements-based Designs2015In: 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. 

  • 23.
    Marinescu, Raluca
    et al.
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Seceleanu, Cristina
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Le Guen, Helene
    ALL4TEC.
    Pettersson, Paul
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Tools for Model-based Testing of Requirements-based Designs2014Report (Other academic)
    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 paper, 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.

  • 24.
    Marinescu, Raluca
    et al.
    Mälardalen University, School of Innovation, Design and Engineering.
    Seceleanu, Cristina
    Mälardalen University, School of Innovation, Design and Engineering.
    Pettersson, Paul
    Mälardalen University, School of Innovation, Design and Engineering.
    An Integrated Framework for Component-based Analysis of Architectural System Models2012In: Proceedings of the ICTSS 2012 Ph.D. Workshop / [ed] Carsten Weise and Brian Nielsen, 2012, p. 1-6Conference paper (Refereed)
    Abstract [en]

    Verifying architectural models of embedded systems is desirable, since architecture can impact the performance and resource usageof the final system implementation. To fulfill this need, one could thinkof combining formal verification and testing to achieve proofs of systemcorrectness with respect to functional and extra-functional requirements.Our first step to accomplish this goal has concretized in the development of a framework that integrates architectural models described inEast-adl language with component-based model-checking techniques.The framework is supported by a tool called ViTAL, which captures thebehavior of East-adl functions as timed automata models, which canbe formally verified in the Uppaal Port model-checker that exploitsthe components-based semantics at the architectural level. Later, thesame formal models will help generate test-suites to provide support formodel-based testing.

1 - 24 of 24
CiteExportLink to result list
Permanent link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf