mdh.sePublications
Change search
Refine search result
12 51 - 96 of 96
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.
  • 51.
    Johnsen, Andreas
    et al.
    Mälardalen University, School of Innovation, Design and Engineering.
    Lundqvist, Kristina
    Mälardalen University, School of Innovation, Design and Engineering.
    Pettersson, Paul
    Mälardalen University, School of Innovation, Design and Engineering.
    Architecture-Based Regression Verification of AADL SpecificationsManuscript (preprint) (Other academic)
    Abstract [en]

    Design artifacts of dependable embedded systems, and the systems themselves, are subjected to a number of modifications during the development process. Verified artifacts that subsequently are modified must necessarily be re-verified to ensure that no faults have been introduced in response to the modification. We collectively call this type of verification as regression verification. Studies show that regression testing alone consumes a vast amount of the total development cost. This is likely a result of unnecessary verification of parts that are not affected by the modification. In this paper, we propose an architecture-based selective regression verification technique for the development process of dependable embedded systems specified in the Architecture Analysis and Design Language (AADL). The selection of necessary regression verification sequences is based on the concept of specification slicing through System Dependence Graphs (SDGs). This allows for the avoidance of unnecessary re-verification, and thereby unnecessary costs.

  • 52.
    Johnsen, Andreas
    et al.
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Lundqvist, Kristina
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Pettersson, Paul
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Hänninen, Kaj
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Torelm, Martin
    Bombardier Transp., Sweden .
    Experience Report: Evaluating Fault Detection Effectiveness and Resource Efficiency of the Architecture Quality Assurance Framework and Tool2017In: Proceedings - International Symposium on Software Reliability Engineering, ISSRE. Volume 2017, 2017, p. 271-281, article id 8109093Conference paper (Refereed)
    Abstract [en]

    The Architecture Quality Assurance Framework (AQAF) is a theory developed to provide a holistic and formal verification process for architectural engineering of critical embedded systems. AQAF encompasses integrated architectural model checking, model-based testing, and selective regression verification techniques to achieve this goal. The Architecture Quality Assurance Tool (AQAT) implements the theory of AQAF and enables automated application of the framework. In this paper, we present an evaluation of AQAT and the underlying AQAF theory by means of an industrial case study, where resource efficiency and fault detection effectiveness are the targeted properties of evaluation. The method of fault injection is utilized to guarantee coverage of fault types and to generate a data sample size adequate for statistical analysis. We discovered important areas of improvement in this study, which required further development of the framework before satisfactory results could be achieved. The final results present a 100% fault detection rate at the design level, a 98.5% fault detection rate at the implementation level, and an average increased efficiency of 6.4% with the aid of the selective regression verification technique.

  • 53.
    Johnsen, Andreas
    et al.
    Mälardalen University, School of Innovation, Design and Engineering.
    Lundqvist, Kristina
    Mälardalen University, School of Innovation, Design and Engineering.
    Pettersson, Paul
    Mälardalen University, School of Innovation, Design and Engineering.
    Jaradat, Omar
    Mälardalen University, School of Innovation, Design and Engineering.
    Automated Verification of AADL-Specifications Using UPPAAL2012In: Proceedings of the 14th IEEE International Symposium on High Assurance Systems Engineering (HASE), 2012, p. 130-138Conference paper (Refereed)
    Abstract [en]

    The Architecture Analysis and Design Language (AADL) is used to represent architecture design decisions of safety-critical and real-time embedded systems. Due to the far-reaching effects these decisions have on the development process, an architecture design fault is likely to have a significant deteriorating impact through the complete process. Automated fault avoidance of architecture design decisions therefore has the potential to significantly reduce the cost of the development while increasing the dependability of the end product. To provide means for automated fault avoidance when developing systems specified in AADL, a formal verification technique has been developed to ensure completeness and consistency of an AADL specification as well as its conformity with the end product. The approach requires the semantics of AADL to be formalized and implemented. We use the methodology of semantic anchoring to contribute with a formal and implemented semantics of a subset of AADL through a set of transformation rules to timed automata constructs. In addition, the verification technique, including the transformation rules, is validated using a case study of a safety-critical fuel-level system developed by a major vehicle manufacturer.

  • 54.
    Johnsen, Andreas
    et al.
    Mälardalen University, School of Innovation, Design and Engineering.
    Pettersson, Paul
    Mälardalen University, School of Innovation, Design and Engineering.
    Lundqvist, Kristina
    Mälardalen University, School of Innovation, Design and Engineering.
    An Architecture-Based Verification Technique for AADL Specifications2011Conference paper (Refereed)
    Abstract [en]

    Quality assurance processes of software-intensive systems are an increasing challenge as the complexity of these systems dramatically increases. The use of Architecture Description Languages (ADLs) provide an important basis for evaluation. The Architecture Analysis and Design Language (AADL) is an ADL developed for designing software intensive systems. In this paper, we propose an architecture-based verification technique covering the entire development process by adapting a combination of model-checking and model-based testing approaches to AADL specifications. The technique reveals inconsistencies of early design decisions and ensures a system's conformity with its AADL specification. The objective and criteria (test-selection) of the verification technique is derived from traditional integration testing.

  • 55.
    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.

  • 56.
    Kang, Eun-Young
    et al.
    Mälardalen University, School of Innovation, Design and Engineering. University of Namur, Belgium.
    Schnobbens, Pierre Yves
    University of Namur, Belgium.
    Pettersson, Paul
    Mälardalen University, School of Innovation, Design and Engineering.
    Verifying functional behaviors of automotive products in EAST-ADL2 using UPPAAL-PORT2011In: Computer Safety, Reliability, and Security: 30th International Conference,SAFECOMP 2011, Naples, Italy, September 19-22, 2011. Proceedings, 2011, p. 243-256Conference paper (Refereed)
    Abstract [en]

    We study the use of formal modeling and verification techniques at an early stage in the development of safety-critical automotive products which are originally described in the domain specific architectural language EAST-ADL2. This architectural language only focuses on the structural definition of functional blocks. However, the behavior inside each functional block is not specified and that limits formal modeling and analysis of systems behaviors as well as efficient verification of safety properties. In this paper, we tackle this problem by proposing one modeling approach, which formally captures the behavioral execution inside each functional block and their interactions, and helps to improve the formal modeling and verification capability of EAST-ADL2: the behavior of each elementary function of EAST-ADL2 is specified in UPPAAL Timed Automata. The formal syntax and semantics are defined in order to specify the behavior model inside EAST-ADL2 and their interactions. A composition of the functional behaviors is considered a network of Timed Automata that enables us to verify behaviors of the entire system using the UPPAAL model checker. The method has been demonstrated by verifying the safety of the Brake-by-wire system design.

  • 57.
    Ke, Xu
    et al.
    University of Southern Denmark.
    Pettersson, Paul
    Mälardalen University, School of Innovation, Design and Engineering.
    Sierszecki, Krzysztof
    University of Southern Denmark.
    Angelov, Christo
    University of Southern Denmark.
    Verification of COMDES-II Systems Using UPPAAL with Model Transformation2008In: 14th International IEEE Conference on Embedded and Real-Time Computing Systems and Applications (RTCSA), Kaohsiung, Taiwan, 2008, p. 153-160Conference paper (Refereed)
    Abstract [en]

    COMDES-II is a component-based software framework intended for model-integrated development of embedded control systems with hard real-time constraints. It provides various kinds of component models to address critical domain-specific issues, such as real-time concurrency and communication in a timed multitasking environment, modal continuous operation combining reactive control behavior with continuous data processing, etc., by following the principle of separation-of-concerns. In the paper we present a transformational approach to the formal verification of both timing and reactive behaviors of COMDES-II systems using UPPAAL, based on a semantic anchoring methodology. The proposed approach adopts UPPAAL timed automata as the semantic units, to which different behavioral concerns of COMDES-II are anchored, such that a COMDES-II system can be precisely specified in UPPAAL, and verified against a set of desired requirements with the preservation of system original operation semantics.

  • 58.
    Koziolek, H.
    et al.
    Industrial Software Systems, ABB Corporate Research Ladenburg, Germany.
    Becker, S.
    University of Paderborn, Germany.
    Happe, J.
    SAP Research, Karlsruhe, Germany.
    Pettersson, Paul
    Mälardalen University, School of Innovation, Design and Engineering.
    Quality of service-oriented software systems (QUASOSS 2010)2011In: Lecture Notes in Computer Science, vol 6627, Berlin: Springer Berlin/Heidelberg, 2011, Vol. 6627 LNCS, p. 364-368Chapter in book (Other academic)
    Abstract [en]

    The 2nd International Workshop on the Quality of Service-Oriented Software Systems (QUASOSS 2010) brought together researchers and practitioners to assess current approaches for analyzing the quality of service-oriented software systems. Due to the current maturation of model-driven methods for service-oriented systems, the declared goal of QUASOSS 2010 was to assess the state-of-the-art, report on successful or unsuccessful application of these methods, and to identify a research roadmap for future approaches. QUASOSS 2010 was attended by 25 participants. It featured a keynote by Prof. Dorina Petriu, 6 paper presentations, and a panel discussion. © 2011 Springer-Verlag Berlin Heidelberg.

  • 59.
    Li, Shuhao
    et al.
    Aalborg University.
    Pettersson, Paul
    Mälardalen University, School of Innovation, Design and Engineering.
    Verification and Controller Synthesis for Resource-Constrained Real-Time Systems: Case Study of an Autonomous Truck2010In: Proceedings of the 15th IEEE International Conference on Emerging Technologies and Factory Automation, ETFA 2010, 2010Conference paper (Refereed)
    Abstract [en]

    An embedded system is often subject to timing constraints, resource constraints, and it should operate properly no matter how its environment behaves. This paper proposes to use timed game automata to characterize the timed behaviors and the environment uncertainties, and use piecewise constant integer functions to approximate the continuous resources in real-time embedded systems. Based on these formal models and techniques, we employ the realtime model checker UPPAAL to verify a given functional and/or timing requirement. In addition, we employ the timed game solver UPPAAL-TIGA to check whether a given control objective can be enforced, and if so, we synthesize a controller for the system. We carry out a case study of this approach on a battery-powered autonomous truck. Experimental results indicate that the method is effective and computationally feasible.

  • 60.
    Lindström, B.
    et al.
    University of Skövde, Skövde, Sweden.
    Andler, S. F.
    University of Skövde, Skövde, Sweden.
    Offutt, J.
    University of Skövde, Skövde, Sweden.
    Pettersson, Paul
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Sundmark, D.
    Swedish Institute of Computer Science, Kista, Sweden.
    Mutating aspect-oriented models to test cross-cutting concerns2015In: 2015 IEEE 8th International Conference on Software Testing, Verification and Validation Workshops, ICSTW 2015 - Proceedings, 2015, p. Article number 7107456-Conference paper (Refereed)
    Abstract [en]

    Aspect-oriented (AO) modeling is used to separate normal behaviors of software from specific behaviors that affect many parts of the software. These are called 'cross-cutting concerns,' and include things such as interrupt events, exception handling, and security protocols. AO modeling allow developers to model the behaviors of cross-cutting concerns independently of the normal behavior. Aspect-oriented models (AOM) are then transformed into code by 'weaving' the aspects (modeling the cross-cutting concerns) into all locations in the code where they are needed. Testing at this level is unnecessarily complicated because the concerns are often repeated in many locations and because the concerns are muddled with the normal code. This paper presents a method to design robustness tests at the abstract, or model, level. The models are mutated with novel operators that specifically target the features of AOM, and tests are designed to kill those mutants. The tests are then run on the implementation level to evaluate the behavior of the woven cross-cutting concerns.

  • 61.
    Lindström, Birgitta
    et al.
    Univ Skövde, Skövde, Sweden..
    Offutt, Jeff
    George Mason Univ, Fairfax, USA..
    Sundmark, Daniel
    Swedish Inst Comp Sci, Kista, Sweden..
    Andler, Sten F.
    Univ Skövde, Skövde, Sweden..
    Pettersson, Paul
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Using mutation to design tests for aspect-oriented models2017In: Information and Software Technology, ISSN 0950-5849, E-ISSN 1873-6025, Vol. 81, p. 112-130Article in journal (Refereed)
    Abstract [en]

    Context: Testing for properties such as robustness or security is complicated because their concerns are often repeated in many locations and muddled with the normal code. Such "cross-cutting concerns" include things like interrupt events, exception handling, and security protocols. Aspect-oriented (AO) modeling allows, developers to model the cross-cutting behavior independently of the normal behavior, thus supporting model-based testing of cross-cutting concerns. However, mutation operators defined for AO programs (source code) are usually not applicable to AO models (AGMs) and operators defined for models do not target the AO features. Objective: We present a method to design abstract tests at the aspect-oriented model level. We define mutation operators for aspect-oriented models and evaluate the generated mutants for an example system. Method: AOMs are mutated with novel operators that specifically target the AO modeling features. Test traces killing these mutant models are then generated. The generated and selected traces are abstract tests that can be transformed to concrete black-box tests and run on the implementation level, to evaluate the behavior of the woven cross-cutting concerns (combined aspect and base models). Results: This paper is a significant extension of our paper at Mutation 2015. We present a complete fault model, additional mutation operators, and a thorough analysis of the mutants generated for an example system. Conclusions: The analysis shows that some mutants are stillborn (syntactically illegal) but none is equivalent (exhibiting the same behavior as the original model). Additionally, our AOM-specific mutation operators can be combined with pre-existing operators to mutate code or models without any overlap.

  • 62.
    Lindström, Birgitta
    et al.
    University of Skövde, Sweden.
    Pettersson, Paul
    Mälardalen University, Department of Computer Science and Electronics.
    Model-Checking with Insufficient Memory Resources2006Report (Other academic)
    Abstract [en]

    Resource limitations is a major problem in model checking. Space and time requirements of model-checking algorithms grow exponentially with respect to the number of variables and parallel automata of the analyzed model. We present a method that is the result of experiences from a case study. It has enabled us to analyze models with much bigger state-spaces than what was possible without our method. The basic idea is to build partitions of the state-space of an analyzed system by iterative invocations of a model-checker. In each iteration the partitions are extended to represent a larger part of the state space, and if needed the partitions are further partitioned. Thereby the analysis problem is divided into a set of subproblems that can be analyzed independently of each other. We present how the method, implemented as a meta algorithm on-top

    of the Uppaal tool, has been applied in the case study.

  • 63.
    Lindström, Birgitta
    et al.
    University of Skövde.
    Pettersson, Paul
    Mälardalen University, Department of Computer Science and Electronics.
    Offutt, Jeff
    George Mason University, Fairfax, United States .
    Generating Trace-Sets for Model-based Testing2007In: Proceedings of the 18th IEEE International Symposium on Software Reliability, 2007, p. 171-180Conference paper (Refereed)
    Abstract [en]

    Model-checkers are powerful tools that can find individual traces through models to satisfy desired properties. These traces provide solutions to a number of problems. Instead of individual traces, software testing needs sets of traces that satisfy coverage criteria. Finding a trace set in a large model is difficult because model checkers generate single traces and use a lot of memory. Space and time requirements of model-checking algorithms grow exponentially with respect to the number of variables and parallel automata of the model being analyzed. We present a method that generates a set of traces by iteratively invoking a model checker. The method mitigates the memory consumption problem by dynamically building partitions along the traces. This method was applied to a testability case study, and it generated the complete trace set, while ordinary model-checking could only generate 26%. 

  • 64.
    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.

  • 65.
    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.

  • 66.
    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. 

  • 67.
    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.

  • 68.
    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.

  • 69.
    Pettersson, Paul
    Mälardalen University, School of Innovation, Design and Engineering.
    Formal Methods Applied in Industry On the Commercialisation of the UPPAAL tool2011In: 2011 35TH IEEE ANNUAL INTERNATIONAL COMPUTER SOFTWARE AND APPLICATIONS CONFERENCE (COMPSAC), 2011, p. 450-451Conference paper (Refereed)
    Abstract [en]

    UPPAAL is a model-checking tool primarily aimed for real-time and embedded systems in which timing plays an important role. It has existed for over 16 years and has become very popular among formal method scientists in academia. In recent years, licenses of the tool have also been offered and sold on commercial basis. In this paper, the characteristics of the tool, its domains of application, as well as some lessons learned from commercializing the tool are described.

  • 70.
    Pettersson, Paul
    et al.
    Mälardalen University, School of Innovation, Design and Engineering.
    Seceleanu, CristinaMälardalen University, School of Innovation, Design and Engineering.
    Proceedings of the 23rd Nordic Workshop on Programming Theory: October 26-28, 2011, Västerås, Sweden2011Conference proceedings (editor) (Other academic)
    Abstract [en]

    The objective of the Nordic Workshop on Programming Theory is to bring together researchers from (but not limited to) the Nordic and Baltic countries interested in programming theory, in order to improve mutual contacts and cooperation. The 23rd Nordic Workshop on Programming Theory took place at Malardalen University, Sweden, 26-28 October 2011. The previous workshops were held in Uppsala (1989, 1999, and 2004), Aalborg (1990), Goteborg (1991 and 1995), Bergen (1992 and 2000), Abo (1993, 1998, 2003, and 2010), Aarhus (1994), Oslo (1996 and 2007), Tallinn (1997, 2002 and 2008), Lyngby (2001 and 2009), Copenhagen (2005), and Reykjavk (2006). There were 36 regular presentations at the workshop. In addition, the following four invited speakers gave presentations: Werner Damm (University of Oldenburg and OFFIS, Germany), Bjorn Lisper (Malardalen University, Sweden), Michael Williams (Ericsson AB, Sweden), and Glynn Winskel (University of Cambridge, United Kingdom).

  • 71.
    Pettersson, Paul
    et al.
    Mälardalen University, School of Innovation, Design and Engineering.
    Seceleanu, Cristina
    Mälardalen University, School of Innovation, Design and Engineering.
    Vulgarakis, Aneta
    Mälardalen University, School of Innovation, Design and Engineering.
    REMES: A Resource Model for Embedded Systems2008Report (Other academic)
    Abstract [en]

    n this paper, we introduce the model REMES for formal modeling and analysis of embedded resources such as storage, power, communication, and computation. The model is annotated with both discrete and continuous resources. It is in fact a state-machine based behavioral language with support for hierarchalmodeling, continuous time, and a notion of explicit entry and exit points, making it suitable for component-based modeling. The analysis of REMES-based systems is centered around a weighted sum in which the variables represent the amounts of consumed resources. We describe a number of important resource related analysis problems, including feasibility, trade-off, and optimal resource-utilization analysis. To formalize these problems, and to provide a basis for formal analysis, we show how to analyze REMES models using the framework of priced timed automata and weighted CTL. To illustrate the approach, we describe a case study in which it has been applied to model and analyze resource usage of a temperature control system. 

  • 72.
    Rodriguez-Navas, Guillermo
    et al.
    Universitat de les Illes Balears, Spain.
    Proenza, Julian
    Universitat de les Illes Balears, Spain.
    Hansson, Hans
    Mälardalen University, School of Innovation, Design and Engineering.
    Pettersson, Paul
    Mälardalen University, School of Innovation, Design and Engineering.
    Using Timed Automata for Modeling the Clocks of Distributed Embedded Systems2010In: Behavioral Modeling for Embedded Systems and Technologies: Applications for Design and Implementation, IGI Global, 2010, p. 172-193Chapter in book (Other academic)
    Abstract [en]

    Model checking is a widely used technique for the formal verification of computer systems. However, the suitability of model checking strongly depends on the capacity of the system designer to specify a model that captures the real behaviour of the system under verification. For the case of real-time systems, this means being able to realistically specify not only the functional aspects, but also the temporal behaviour of the system. This chapter is dedicated to modeling clocks in distributed embedded systems using the timed automata formalism. The different types of computer clocks that may be used in a distributed embedded system and their effects on the temporal behaviour of the system are introduced, together with a systematic presentation of how the behaviour of each kind of clock can be modeled. The modeling is particularized for the UPPAAL model checker, although it can be easily adapted to other model checkers based on the theory of timed automata.

  • 73.
    Seceleanu, Cristina Cerschi
    et al.
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Johansson, M.
    ABB Corporate Research, Sweden.
    Suryadevara, J.
    Volvo Construction Equipment, Sweden.
    Sapienza, Gaetana
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems. ABB Corporate Research, Sweden.
    Seceleanu, Tiberiu
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems. ABB Corporate Research, Sweden.
    Ellevseth, S. -E
    ABB Corporate Research, Norway.
    Pettersson, Paul
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Analyzing a wind turbine system: From simulation to formal verification2017In: Science of Computer Programming, ISSN 0167-6423, E-ISSN 1872-7964, Vol. 133, p. 216-242Article in journal (Refereed)
    Abstract [en]

    Many industrial systems are hybrid by nature, most often being made of a discrete controller that senses and regulates the execution of a plant characterized by continuous dynamics. Examples of such systems include wind turbines that convert wind energy into electrical energy. Designing industrial control systems is challenging, due to the mixed nature of requirements (functional, timing, etc.) as well as due to the complexity stemming from the interaction of the controller with the plant. Model-based techniques help in tackling the design challenges, whereas methods such as simulation with tools like MATLAB/Simulink can be employed for analysis. Although practical, these methods alone cannot ensure full predictability, due to the fact that they cannot guarantee system properties for all possible executions of the system model. In order to ensure that the system will behave as expected under any operational circumstance, formal verification and validation procedures need to be added to the actual development process. In this paper, we propose an extension of the iFEST (industrial Framework for Embedded Systems Tools) process and platform for embedded systems design with model-based testing using MaTeLo, and model checking time-dependent requirements with the UPPAAL tool, as means of increasing the confidence in the system's behavior. To show the feasibility of the techniques on industrially-sized systems, we analyze a wind turbine industrial prototype model against functional and timing requirements. We capture the execution semantics of the plant and controller components of the wind turbine via logical clocks and constraints expressed in the clock constraint specification language (CCSL) of UML MARTE, after which we construct real-time models amenable to model checking, by mapping the timed behavior (expressed in CCSL) of the real-time components of the wind turbine, onto timed automata. Our work is a first application on an industrial wind turbine system of complementary methods for formal analysis, that is, model-based testing, and model checking a mathematically tractable system abstraction based on data obtained by simulating the system with MATLAB/Simulink. We also discuss relevant modeling and verification challenges encountered during our experiences with the wind turbine system.

  • 74.
    Seceleanu, Cristina
    et al.
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Pettersson, Paul
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Foreword2015In: JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING, ISSN 2352-2208, Vol. 84, no 1, p. 1-1Article in journal (Other academic)
  • 75.
    Seceleanu, Cristina
    et al.
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Pettersson, PaulMälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Journal of Logical and Algebraic Methods in Programming: NWPT 2011 Special Issue2015Conference proceedings (editor) (Other academic)
  • 76.
    Seceleanu, Cristina
    et al.
    Mälardalen University, School of Innovation, Design and Engineering.
    Pettersson, Paul
    Mälardalen University, School of Innovation, Design and Engineering.
    Hansson, Hans
    Mälardalen University, School of Innovation, Design and Engineering.
    Scheduling Timed Modules for Correct Resource Sharing2008In: Proceedings of the 1st International Conference on Software Testing, Verification and Validation, ICST 2008, 2008, p. 102-111Conference paper (Refereed)
    Abstract [en]

    Real-time embedded systems typically include concurrent tasks of different priorities with time-dependent operations accessing common resources. In this context, unsynchronized

    parallel executions may lead to hazard situations caused by e.g., race conditions. To be able to detect such

    faulty system behaviors before implementation, we introduce a unified model of resource constrained, scheduled

    real-time system descriptions, in Alur's and Henzinger's rigorous framework of timed reactive modules. We take a

    component-based design perspective and construct the real-time system model, by refinement, as a composition of real-time periodic preemptible tasks with encoded functionality,

    and a fixed-priority scheduler, all modeled as timed modules.

    For the model, we express the notions of race condition and redundant locking, formally, as invariance properties

    that can be verified by model-checking.

  • 77.
    Seceleanu, Cristina
    et al.
    Mälardalen University, School of Innovation, Design and Engineering.
    Vulgarakis, Aneta
    Mälardalen University, School of Innovation, Design and Engineering.
    Pettersson, Paul
    Mälardalen University, School of Innovation, Design and Engineering.
    REMES: A Resource Model for Embedded Systems2009In: In Proc. of the 14th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS 2009), IEEE Computer Society, 2009, p. 84-94Conference paper (Refereed)
    Abstract [en]

    In this paper, we introduce the model REMES for formal modeling and analysis of embedded resources such as storage,energy, communication, and computation. The model is a state-machine based behavioral language with support for hierarchical modeling, resource annotations, continuous time, and notions of explicit entry and exit points that make it suitable for component-based modeling of embedded systems.The analysis of REMES-based systems is centered around a weighted sum in which the variables represent the amounts of consumed resources. We describe a numberof important resource related analysis problems, including feasibility, trade-off, and optimal resource-utilization analysis.To formalize these problems and provide a basis for rigorous analysis, we show how to analyze REMES models using the framework of priced timed automata and weightedCTL. To illustrate the approach, we describe a case study inwhich it has been applied to model and analyze resource usageof a temperature control system.

  • 78.
    Sentilles, Séverine
    et al.
    Mälardalen University, School of Innovation, Design and Engineering.
    Pettersson, Anders
    Mälardalen University, School of Innovation, Design and Engineering.
    Nyström, Dag
    Mälardalen University, School of Innovation, Design and Engineering.
    Nolte, thomas
    Mälardalen University, School of Innovation, Design and Engineering.
    Pettersson, Paul
    Mälardalen University, School of Innovation, Design and Engineering.
    Crnkovic, Ivica
    Mälardalen University, School of Innovation, Design and Engineering.
    Save-IDE – A Tool for Design, Analysis andImplementation of Component-based Embedded Systems2009In: 2009 31ST INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING, PROCEEDINGS, IEEE Computer Society , 2009, p. 607-610Conference paper (Refereed)
    Abstract [en]

    The paper presents Save-IDE, an Integrated Development Environment for thedevelopment of component-based embedded systems. Save-IDE supports efficient development of dependable embedded systems by providing tools for design of embedded software systems using a dedicated component model, formal specification and analysis of component and system behaviors already in early development phases, and a fully automated transformation of the system of components into an executable image.

  • 79.
    Sentilles, Séverine
    et al.
    Mälardalen University, School of Innovation, Design and Engineering.
    Pettersson, Paul
    Mälardalen University, School of Innovation, Design and Engineering.
    Crnkovic, Ivica
    Mälardalen University, School of Innovation, Design and Engineering.
    Håkansson, John
    Uppsala University.
    Save-IDE - An Integrated development environment for building predictable component-based embedded systems2008In: Proceedings of the 23rd IEEE/ACM International Conference on Automated Software Engineering (ASE 2008), L'Aquila, Italy, 2008, p. 493-494Conference paper (Refereed)
    Abstract [en]

    In this paper we present an Integrated Development Environment Save-IDE, a toolset that embraces several tools: a tool for designing component-based systems and components, modeling and predicting certain run-time properties, such as timing properties, and transforming the components to real-time execution elements. Save-IDE is specialized for the domain of dependable embedded systems, which in addition to standard design tools requires tool support for analysis and verification of particular properties of such systems.

  • 80.
    Slutej, Davor
    et al.
    Mälardalen University, School of Innovation, Design and Engineering.
    Håkansson, J.
    Uppsala University.
    Suryadevara, Jagadish
    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.
    Analyzing a Pattern-Based Model of a Real-Time Turntable System.2009In: Electronical Notes in Theoretical Computer Science, ISSN 1571-0661, E-ISSN 1571-0661, Vol. 1, no 6, p. 161-178Article in journal (Refereed)
    Abstract [en]

    Designers of industrial real-time systems are commonly faced with the problem of complex system modeling and analysis, even if a component-based design paradigm is employed. In this paper, we present a case-study in formal modeling and analysis of a turntable system, for which the components are described in the SaveCCM language. The search for general principles underlying the internal structure of our real-time system has motivated us to propose three modeling patterns of common behaviors of real-time components, which can be instantiated in appropriate design contexts. The benefits of such reusable patterns are shown in the case-study, by allowing us to produce easy-to-read and manageable models for the real-time components of the turntable system. Moreover, we believe that the patterns may pave the way toward a generic pattern-based modeling framework targeting real-time systems in particular.

  • 81.
    Suryadevara, Jagadish
    et al.
    Mälardalen University, School of Innovation, Design and Engineering.
    Kang, Eun-Young
    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.
    Bridging the Semantic Gap between Abstract Models of Embedded Systems2010In: Lecture Notes in Computer Science, vol. 6902, Springer, 2010, p. 55-73Chapter in book (Refereed)
    Abstract [en]

    In the development of embedded software, modeling languages used within or across development phases e.g., requirements, specification, design, etc are based on different paradigms and an approach for relating these is needed. In this paper, we present a formal framework for relating specification and design models of embedded systems. We have chosen UML statemachines as specification models and ProCom component language for design models. While the specification is event-driven, the design is based on time triggering and data ow. To relate these abstractions, through the execution trajectories of corresponding models, formal semantics for both kinds of models and a set of inference rules are defined. The approach is applied on an autonomous truck case-study.

  • 82.
    Suryadevara, Jagadish
    et al.
    Mälardalen University, School of Innovation, Design and Engineering.
    Pettersson, Paul
    Mälardalen University, School of Innovation, Design and Engineering.
    Seceleanu, Cristina
    Mälardalen University, School of Innovation, Design and Engineering.
    Validating the Design Model of an Autonomous Truck System2009Conference paper (Refereed)
    Abstract [en]

    Model driven approaches have become effective solutions for the development of embedded systems. In particular, models across various abstraction layers, e.g., application, design, and implementation, provide the opportunity for applying different analysis techniques appropriate at various phases of system development. In this paper, we informally show how to validate the design model of an {em Autonomous Truck} embedded system, by comparing its trajectories with the trajectories of the corresponding application model. In the comparison, we also correlate the corresponding time scales of the two different models. The autonomous truck system is designed in the integrated modeling environment of SaveIDE. The system's functional and timing requirements verification is carried out on the truck's design model. Our work can be regarded as a preliminary step towards developing a general solution to the problem of bridging the gap between application and design models of embedded systems.

  • 83.
    Suryadevara, Jagadish
    et al.
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Sapienza, Gaetana
    ABB Corporate Research, Norway.
    Seceleanu, Cristina
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Seceleanu, Tiberiu
    ABB Corporate Research, Norway.
    Elleveseth, Stein-Erik
    ABB Corporate Research, Norway.
    Pettersson, Paul
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Wind Turbine System: An Industrial Case Study in Formal Modeling and Verification2014In: Communications in Computer and Information Science, Volume 419 CCIS, 2014, p. 229-245Conference paper (Refereed)
    Abstract [en]

    In the development of embedded systems, the formal analysis of system artifacts, such as structural and behavioral models, helps the system engineers to understand the overall functional and timing behavior of the system. In this case study paper, we present our experience in applying formal verification and validation (V&V) techniques, we had earlier proposed, for an industrial wind turbine system (WTS). We demonstrate the complementary benefits of formal verification in the context of existing V&V practices largely based on simulation and testing. We also discuss some modeling trade-offs and challenges we have identified with the case-study, which are worth being emphasized. One issue is related, for instance, to the expressiveness of the system artifacts, in view of the known limitations of rigorous verification, e.g. model-checking, of industrial systems.

  • 84.
    Suryadevara, Jagadish
    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.
    Mallet, F.
    Aoste Team-project INRIA/I3S, Sophia-Antipolis, France.
    Pettersson, Paul
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Verifying MARTE/CCSL mode behaviors using UPPAAL2013In: Lect. Notes Comput. Sci., 2013, p. 1-15Conference paper (Refereed)
    Abstract [en]

    In the development of safety-critical embedded systems, the ability to formally analyze system behavior models, based on timing and causality, helps the designer to get insight into the systems overall timing behavior. To support the design and analysis of real-time embedded systems, the UML modeling profile MARTE provides CCSL - a time model and a clock constraint specification language. CCSL is an expressive language that supports specification of both logical and chronometric constraints for MARTE models. On the other hand, semantic frameworks such as timed automata provide verification support for real-time systems. To address the challenge of verifying CCSL-based behavior models, in this paper, we propose a technique for transforming MARTE/CCSL mode behaviors into Timed Automata for model-checking using the UPPAAL tool. This enables verification of both logical and chronometric properties of the system, which has not been possible before. We demonstrate the proposed transformation and verification approach using two relevant examples of real-time embedded systems.

  • 85.
    Suryadevara, Jagadish
    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.
    Mallet, Frederic
    Univ. of Nice .
    Pettersson, Paul
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Software Engineering and Formal Methods2013In: Software Engineering and Formal Methods: 11th International Conference, SEFM 2013, Madrid, Spain, September 25-27, 2013. Proceedings, Springer, 2013, p. 1-15Chapter in book (Refereed)
    Abstract [en]

    In the development of safety-critical embedded systems, the ability to formally analyze system behavior models, based on timing and causality, helps the designer to get insight into the system’s overall timing behavior. To support the design and analysis of real-time embedded systems, the UML modeling profile MARTE provides CCSL – a time model and a clock constraint specification language. On the one hand, CCSL is an expressive language that supports specification of both logical and chronometric constraints associated with MARTE models. On the other hand, semantic frameworks such as Timed Automata provide verification support for real-time systems. To tackle the challenge of verifying CCSL-based system properties, in this paper, we propose a technique for transforming MARTE/CCSL mode behaviors into Timed Automata for model-checking using the UPPAAL tool. This enables verification of both logical and chronometric properties of the system, which has not been possible before. We demonstrate the proposed transformation and verification approach using two relevant examples of real-time embedded systems.

  • 86.
    Suryadevara, Jagadish
    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.
    Pattern-driven support for designing component-based architectural models.2011In: 18TH IEEE INTERNATIONAL CONFERENCE AND WORKSHOPS ON ENGINEERING OF COMPUTER BASED SYSTEMS (ECBS 2011) / [ed] Sprinkle, J; Sterritt, R; Breitman, K, 2011, p. 187-196Conference paper (Refereed)
    Abstract [en]

    The development of embedded systems often requires the use of various models such as requirements specification, architectural (component-based), and deployment models, across different phases. However, there exists little design support for obtaining suitable component-based designs that satisfy specified requirements and timing constraints. In order to provide guided support for the design process of embedded systems, we introduce several component templates, referred as patterns, which we also formally verify against relevant properties. To illustrate the usefulness of the approach, we have applied the proposed patterns to obtain a component-based design of a temperature control system.

  • 87.
    Suryadevara, Jagadish
    et al.
    Mälardalen University, School of Innovation, Design and Engineering.
    Vulgarakis, Aneta
    Mälardalen University, School of Innovation, Design and Engineering.
    Carlson, Jan
    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.
    ProCom: Formal Semantics2009Report (Other (popular science, discussion, etc.))
    Abstract [en]

    This technical report presents the formal semantics of the ProCom component model.

  • 88.
    Vulgarakis, Aneta
    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.
    Skuliber, Ivan
    Ericsson Nikola Tesla, Zagreb, Croatia .
    Huljenić, Darko
    Ericsson Nikola Tesla, Zagreb, Croatia.
    Validation of embedded systems behavioral models on a component-based Ericsson Nikola Tesla demonstrator2011In: Proceedings - International Conference on Quality Software, 2011, p. 156-165Conference paper (Refereed)
    Abstract [en]

    Embedded systems are challenging to design, due to the implementation platform constraints that have to be considered, preferably from early stages of design, next-by system functionality. Hence, embedded system models need to be timing and resource-aware, to make formal verification of extra functional properties applicable at high levels of abstraction. In most cases, a frequent obstacle to the successful application of such rigorous techniques is the lack of the proposed models'validation against real-world application measurements. In this paper, we show how to model extra-functional behavior, and verify the resulted behavioral models of a component-based Ericsson Nikola Tesla prototype telecommunications system. The models are described in our recently introduced REMES language, with Priced Timed Automata semantics that allows us to apply UPPAAL -based tools for model-checking the system'sresponse time and compute optimal resource usage traces. The validation of our models is ensured by using actual values of timing, CPU, and memory usage in our models, measured by Ericsson researchers on the prototype's source code. © 2011 IEEE.

  • 89.
    Vulgarakis, Aneta
    et al.
    Mälardalen University, School of Innovation, Design and Engineering.
    Suryadevara, Jagadish
    Mälardalen University, School of Innovation, Design and Engineering.
    Carlson, Jan
    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.
    Formal semantics of the ProCom real-time component model2009In: Proceedings of the 35th Euromicro Conference on Software Engineering and Advanced Applications 2009. SEAA 09, 2009, p. 478-485Conference paper (Refereed)
    Abstract [en]

    ProCom is a new component model for real-timeand embedded systems, targeting the domains of vehicularand telecommunication systems. In this paper, we describehow the architectural elements of the ProCom componentmodel have been given a formal semantics. The semantics isgiven in a small but powerful finite state machine formalism,with notions of urgency, timing, and priorities. By definingthe semantics in this way, we (i) provide a rigorous and compactdescription of the modeling elements of ProCom, (ii) setthe ground for formal analysis using other formalisms, and(iii) provide an intuitive and useful description for bothpractitioners and researchers. To illustrate the approach,we exemplify with a number of particularly interestingcases, ranging from ports and services to components andcomponent hierarchies.

  • 90.
    Åkerholm, Mikael
    et al.
    Mälardalen University, Department of Computer Science and Electronics.
    Carlson, Jan
    Mälardalen University, Department of Computer Science and Electronics.
    Fredriksson, Johan
    Mälardalen University, Department of Computer Science and Electronics.
    Hansson, Hans
    Mälardalen University, Department of Computer Science and Electronics.
    Håkansson, John
    Uppsala University, Sweden.
    Möller, Anders
    Mälardalen University, Department of Computer Science and Electronics.
    Pettersson, Paul
    Uppsala University, Sweden.
    Tivoli, Massimo
    University of L'Aquila, Italy.
    The SAVE approach to component-based development of vehicular systems2007In: Journal of Systems and Software, ISSN 0164-1212, E-ISSN 1873-1228, Vol. 80, no 5, p. 655-667Article in journal (Refereed)
    Abstract [en]

    The component-based strategy aims at managing complexity, shortening time-to-market, and reducing maintenance requirements by building systems with existing components. The full potential of this strategy has not yet been demonstrated for embedded software, mainly because of specific requirements in the domain, e.g., those related to timing, dependability, and resource consumption. We present SaveCCT - a component technology intended for vehicular systems, show the applicability of SaveCCT in the engineering process, and demonstrate its suitability for vehicular systems in an industrial case-study. Our experiments indicate that SaveCCT provides appropriate expressiveness, resource efficiency, analysis and verification support for component-based development of vehicular software. 

  • 91.
    Åkerholm, Mikael
    et al.
    Mälardalen University, Department of Computer Science and Electronics.
    Carlson, Jan
    Mälardalen University, Department of Computer Science and Electronics.
    Fredriksson, Johan
    Mälardalen University, Department of Computer Science and Electronics.
    Hansson, Hans
    Mälardalen University, Department of Computer Science and Electronics.
    Sjödin, Mikael
    Mälardalen University, Department of Computer Science and Electronics.
    Nolte, Thomas
    Mälardalen University, Department of Computer Science and Electronics.
    Håkansson, John
    Mälardalen University, Department of Computer Science and Electronics.
    Pettersson, Paul
    Mälardalen University, Department of Computer Science and Electronics.
    Handling Subsystems using the SaveComp Component Technology2006In: Workshop on Models and Analysis for Automotive Systems (WMAAS'06) in conjunction with the 27th IEEE Real-Time Systems Symposium (RTSS'06), Rio de Janeiro, Brazil, 2006Conference paper (Refereed)
  • 92.
    Åkerholm, Mikael
    et al.
    Mälardalen University, Department of Computer Science and Electronics.
    Carlson, Jan
    Mälardalen University, Department of Computer Science and Electronics.
    Håkansson, John
    Uppsala University, Uppsala, Sweden.
    Hansson, Hans
    Mälardalen University, Department of Computer Science and Electronics.
    Sjödin, Mikael
    Mälardalen University, Department of Computer Science and Electronics.
    Nolte, Thomas
    Mälardalen University, Department of Computer Science and Electronics.
    Pettersson, Paul
    Mälardalen University, Department of Computer Science and Electronics.
    The SaveCCM Language Reference Manual2007Report (Other academic)
    Abstract [en]

    This language reference describes the syntax and semantics of SaveCCM, a

    component modeling language for embedded systems designed with vehicle applications and safety concerns in focus. The SaveCCM component model was

    defined within the SAVE project. The SAVE components are influenced mainly

    by the Rubus component technology, with a switch concept similar to that

    in Koala. The semantics is defined by a transformation into timed automata

    with tasks, a formalism that explicitly models timing and real-time task scheduling.

    The purpose of this document is to describe a semantics of the SAVE component modeling language, which can be used to describe timing and functional behavior of components. The model of a system is in some cases an over approximation of the actual system behavior. An implementation of a model can resolve non-determinism e.g. by merging tasks or assigning a scheduling policy (such as static scheduling or fixed priority, preemptive or not) that will resolve

    the non-determinism.

  • 93.
    Åsberg, Mikael
    et al.
    Mälardalen University, School of Innovation, Design and Engineering.
    Nolte, Thomas
    Mälardalen University, School of Innovation, Design and Engineering.
    Pettersson, Paul
    Mälardalen University, School of Innovation, Design and Engineering.
    Prototyping and Code Synthesis of Hierarchically Scheduled Systems using TIMES2010In: FTRA Journal of Convergence, ISSN 2093-7741, Vol. 1, no 1, p. 75-84Article in journal (Refereed)
    Abstract [en]

    In hierarchical scheduling a system is organized as a tree of nodes, where each node schedules its child nodes. A node contains tasks and/or subsystems, where a subsystem is typically developed by a development team. Given a system where each part is subcontracted to different developers, they can benefit from hierarchical scheduling by parallel development and simplified integration of subsystems. Each team should have the possibility to test their system before integration. Hence, we show how a node, in a hierarchical scheduling tree, can be analyzed in the Times tool by replacing all interference from nodes with a small set of higher priority tasks. We show an algorithm that can generate these tasks, including their parameters. Further, we use the Times code-generator, in combination with operating system extensions, to generate source code that emulates the scheduling environment for a subsystem, in an arbitrary level in the tree. Our experiments include two example systems. In the first case we generate source code for an industrial oriented platform (VxWorks) and conduct a performance evaluation. In the second example we generate source code that emulates the scheduling environment for a video application, running in Linux, and we perform a frame-rate evaluation.

  • 94.
    Åsberg, Mikael
    et al.
    Mälardalen University, School of Innovation, Design and Engineering.
    Nolte, Thomas
    Mälardalen University, School of Innovation, Design and Engineering.
    Pettersson, Paul
    Mälardalen University, School of Innovation, Design and Engineering.
    Prototyping Hierarchically Scheduled Systems using Task Automata and TIMES2010In: Proceedings of the 5th International Conference on Embedded and Multimedia Computing (EMC-10), 2010, p. article nr: 5575626-Conference paper (Refereed)
    Abstract [en]

    In hierarchical scheduling, a system is organized into multiple levels of individually scheduled subsystems (hierarchical scheduling tree), which provides several benefits for developers including possibilities for parallel development of subsystems. In this paper, we study how the model of task automata and the Times tool can be applied to provide support for rapid and early prototyping of hierarchically scheduled embedded systems. As a main result, we show how a single node, in an arbitrary level in a hierarchical scheduling tree (scheduled with fixed-priority preemptive scheduling), can easily be analyzed in Times by replacing all interfering nodes with a small set of higher priority (dummy) tasks. We show with an algorithm how these dummy tasks are generated (including task-parameters such as period, offset etc.). Further, we generate executable source code, with the Times code-generator, that emulates the scheduling environment (with our dummy tasks), i.e., the hierarchical scheduling tree and all of its preemptions, of a small example system. Yet another contribution is that we transform the generated (brickOS) source code to run on an industrial oriented platform (VxWorks), and conduct an performance evaluation.

  • 95.
    Åsberg, Mikael
    et al.
    Mälardalen University, School of Innovation, Design and Engineering.
    Pettersson, Paul
    Mälardalen University, School of Innovation, Design and Engineering.
    Nolte, Thomas
    Mälardalen University, School of Innovation, Design and Engineering.
    Evaluating the Run-Time Performance of Synthesised Resource-Reservation Schedulers Using TAtoC, UPPAAL and Frama-C2013Report (Other academic)
  • 96.
    Åsberg, Mikael
    et al.
    Mälardalen University, School of Innovation, Design and Engineering.
    Pettersson, Paul
    Mälardalen University, School of Innovation, Design and Engineering.
    Nolte, Thomas
    Mälardalen University, School of Innovation, Design and Engineering.
    Modelling, Verification and Synthesis of Two-Tier Hierarchical Fixed-Priority Preemptive Scheduling2011In: Proceedings - 23rd EUROMICRO Conference on Real-Time Systems (ECRTS'11), 2011, p. 172-181Conference paper (Refereed)
    Abstract [en]

    Hierarchical scheduling has major benefits when it comes to integrating hard real-time applications. One of those benefits is that it gives a clear runtime separation of applications in the time domain. This in turn gives a protection against timing error propagation in between applications. However, these benefits rely on the assumption that the scheduler itself schedules applications correctly according to the scheduling parameters and the chosen scheduling policy. A faulty scheduler can affect all applications in a negative way. Hence, being able to guarantee that the scheduler is correct is of great importance. Therefore, in this paper, we study how properties of hierarchical scheduling can be verified. We model a hierarchically scheduled system using task automata, and we conduct verification with model checking using the Times tool. Further, we generate C-code from the model and we execute the hierarchical scheduler in the Vx Works kernel. The CPU and memory overhead of the modelled scheduler is compared against an equivalent manually coded two-level hierarchical scheduler. We show that the worst-case memory consumption is similar and that there is a considerable difference in CPU overhead.

12 51 - 96 of 96
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