mdh.sePublications
Change search
CiteExportLink to record
Permanent link

Direct 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
Model Based Development of Embedded Systems using Logical Clock Constraints and Timed Automata
Mälardalen University, School of Innovation, Design and Engineering. (IS (Formal Modeling and Analysis Group))
2013 (English)Doctoral thesis, comprehensive summary (Other academic)
Abstract [en]

In modern times, human life is intrinsically depending on real-time embedded systems (RTES) with increasingly safety-critical and mission-critical features, for instance, in domains such as automotive and avionics. These systems are characterized by stringent functional requirements and require predictable timing behavior. However, the complexity of RTES has been ever increasing requiring systematic development methods. To address these concerns, model-based frameworks and component-based design methodologies have emerged as a feasible solution. Further, system artifacts such as requirements/specifications, architectural designs as well as behavioral models like statemachine views are integrated within the development process. However, several challenges remain to be addressed, out of which two are especially important: expressiveness, to represent the real-time and causality behavior, and analyzability, to support verification of functional and timing behavior.

As the main research contribution, this thesis presents design and verification techniques for model-based development of RTES, addressing expressiveness and analyzability for architectural and behavioral models. To begin with, we have proposed a systematic design process to support component-based development. Next, we have provided a real-time semantic basis, in order to support expressiveness and verification for structural and behavioral models. This is achieved by defining an intuitive formal semantics for real-time component models, using ProCom, a component model developed at our research centre, and also using the CCSL (Clock Constraint Specification Language), an expressive language for specification of timed causality behavior. This paves the way for formal verification of both architectural and behavioral models, using model checking, as we show in this work, by transforming the models into timed automata and performing verification using UPPAAL, a model checking tool based on timed automata. Finally, the research contributions are validated using representative examples of RTES as well as an industrial case-study.

Place, publisher, year, edition, pages
Västerås: Mälardalen University , 2013.
Series
Mälardalen University Press Dissertations, ISSN 1651-4238 ; 146
Keyword [en]
Embedded Systems, Model-based development, Model-Checking, Architectural Modeling, CCSL, Timed Automata
National Category
Embedded Systems
Identifiers
URN: urn:nbn:se:mdh:diva-22328ISBN: 978-91-7485-123-6 (print)OAI: oai:DiVA.org:mdh-22328DiVA: diva2:665047
Public defence
2013-12-09, Kappa, Mälardalen University, Västerås, 13:15 (English)
Opponent
Supervisors
Projects
ARROWS
Funder
Swedish Research Council, 2270 430 16243
Available from: 2013-11-01 Created: 2013-11-01 Last updated: 2013-11-18Bibliographically approved
List of papers
1. Analyzing a Pattern-Based Model of a Real-Time Turntable System.
Open this publication in new window or tab >>Analyzing a Pattern-Based Model of a Real-Time Turntable System.
Show others...
2009 (English)In: Electronical Notes in Theoretical Computer Science, ISSN 1571-0661, Vol. 1, no 6, 161-178 p.Article in journal (Refereed) Published
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.

National Category
Engineering and Technology
Research subject
Computer Science
Identifiers
urn:nbn:se:mdh:diva-12250 (URN)10.1016/j.entcs.2009.09.034 (DOI)2-s2.0-70349310123 (Scopus ID)
Conference
Formal Foundations of Embedded Software and Component-Based Software Architectures
Projects
PROGRESS
Available from: 2011-05-12 Created: 2011-05-12 Last updated: 2013-12-03Bibliographically approved
2. Formal semantics of the ProCom real-time component model
Open this publication in new window or tab >>Formal semantics of the ProCom real-time component model
Show others...
2009 (English)In: Proceedings of the 35th Euromicro Conference on Software Engineering and Advanced Applications 2009. SEAA 09, 2009, 478-485 p.Conference paper, Published 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.

Keyword
real-time systems; embedded systems; component model, finite state machines; timed automata
Research subject
Computer Science
Identifiers
urn:nbn:se:mdh:diva-6553 (URN)10.1109/SEAA.2009.53 (DOI)000275857500069 ()2-s2.0-74549208521 (Scopus ID)978-076953784-9 (ISBN)
Conference
EUROMICRO2009 - 35th EUROMICRO Conference on Software Engineering and Advanced Applications, SEAA 2009; Patras; 27 August 2009 through 29 August 2009
Projects
PROGRESS
Available from: 2009-07-08 Created: 2009-07-08 Last updated: 2013-12-19Bibliographically approved
3. Pattern-driven support for designing component-based architectural models.
Open this publication in new window or tab >>Pattern-driven support for designing component-based architectural models.
2011 (English)In: 18TH IEEE INTERNATIONAL CONFERENCE AND WORKSHOPS ON ENGINEERING OF COMPUTER BASED SYSTEMS (ECBS 2011) / [ed] Sprinkle, J; Sterritt, R; Breitman, K, 2011, 187-196 p.Conference paper, Published 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.

National Category
Computer and Information Science
Research subject
Computer Science
Identifiers
urn:nbn:se:mdh:diva-12249 (URN)10.1109/ECBS.2011.20 (DOI)000298802400023 ()2-s2.0-80051962547 (Scopus ID)978-0-7695-4379-6 (ISBN)
Conference
18th IEEE International Conference on Engineering of Computer-Based Systems
Projects
ARROWSPROGRESS
Funder
Swedish Research Council, 2270 430 16243
Note

2011 IEEE. Personal use of this material is permitted. Permission from IEEE must be obtained for all other users, including reprinting/ republishing this material for advertising or promotional purposes, creating new collective works for resale or redistribution to servers or lists, or reuse of any copyrighted components of this work in other works

Available from: 2011-05-12 Created: 2011-05-12 Last updated: 2013-12-03Bibliographically approved
4. Analysis support for TADL2 timing constraints on EAST-ADL models
Open this publication in new window or tab >>Analysis support for TADL2 timing constraints on EAST-ADL models
2013 (English)In: Lecture Notes in Computer Science, vol. 7957, Springer, 2013, 89-105 p.Chapter in book (Refereed)
Abstract [en]

It is critical to analyze characteristics of real-time embedded systems, such as timing behavior, early in the development. In the automotive domain, EAST-ADL is a concrete example of the model-based approach for the architectural modeling of real-time systems. The Timing Augmented Description Language v2 (TADL2) allows for the specification of timing constraints on top of EAST-ADL models. In this paper we propose a formal validation & verification methodology for timing behaviors given with TADL2. The formal semantics of the timing constraints is given as a mapping to the Clock Constraint Specification Language (CCSL), a formal language that implements the MARTE Time Model. Based on such a mapping, the validation is carried out by the simulation of TADL2 specifications. The simulation allows for a rapid prototyping of TADL2 specifications. The verification is performed based on a TADL2 mapping to timed automata modeling using the Uppaal model-checker. The whole process is illustrated on a Brake-By-Wire application.

Place, publisher, year, edition, pages
Springer, 2013
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 7957
Series
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 7957
Keyword
Architectural modeling, Automotive domains, Clock constraints, Description languages, Model based approach, Real-time embedded systems, Timing constraints, Verification methodology, Automata theory, Formal languages, Model checking, Rapid prototyping, Real time systems, Software architecture, Specification languages, Specifications, Mapping
National Category
Engineering and Technology
Identifiers
urn:nbn:se:mdh:diva-20823 (URN)10.1007/978-3-642-39031-9_8 (DOI)2-s2.0-84879852991 (Scopus ID)9783642390302 (ISBN)
Conference
7th European Conference on Software Architecture, ECSA 2013, 1 July 2013 through 5 July 2013, Montpellier
Note

7th European Conference on Software Architecture, ECSA 2013; Montpellier; France; 1 July 2013 through 5 July 2013

Available from: 2013-08-02 Created: 2013-08-02 Last updated: 2016-05-17Bibliographically approved
5. Validating EAST-ADL Timing Constraints using UPPAAL
Open this publication in new window or tab >>Validating EAST-ADL Timing Constraints using UPPAAL
2013 (English)In: 39th Euromicro Conference on Software Engineering and Advanced Applications (SEAA), 2013Conference paper, Published paper (Refereed)
Abstract [en]

Systematic and formal development approaches for safety- and mission critical systems are of increasing importance. These systems are often implemented as periodically triggered control systems, to ensure deterministic and analyzable timing behavior. However, integrating timing ‘constraints’ in the development process remains a challenging task. For instance, these constraints itself should be formally verified as consistent and feasible with respect to the system design. In this paper, we present a timed automata based validation approach for EAST-ADL timing constraints for periodic control systems. The constraints are specified using CCSL – the Clock Constraint Specification Language,and transformed into timed automata, to enable formal verification with UPPAAL model-checker. The resulting timed automata specification can be simulated and verified for the formal validation of the timing constraints. Further, the transformed specification model can be easily integrated with the actual system design, thus extending verification aspects. The proposed approach is demonstrated using the timing constraints for an Anti-lock Braking System (ABS) example.

National Category
Engineering and Technology
Identifiers
urn:nbn:se:mdh:diva-21400 (URN)10.1109/SEAA.2013.46 (DOI)2-s2.0-84889061215 (Scopus ID)
Conference
39th Euromicro Conference on Software Engineering and Advanced Applications (SEAA 2013) Santander, Spain September 4-6, 2013
Projects
ARROWS - Design Techniques for Adaptive Embedded Systems
Available from: 2013-09-16 Created: 2013-09-11 Last updated: 2016-06-02Bibliographically approved
6. Software Engineering and Formal Methods
Open this publication in new window or tab >>Software Engineering and Formal Methods
2013 (English)In: Software Engineering and Formal Methods: 11th International Conference, SEFM 2013, Madrid, Spain, September 25-27, 2013. Proceedings, Springer, 2013, 1-15 p.Chapter 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.

Place, publisher, year, edition, pages
Springer, 2013
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 8137
National Category
Engineering and Technology
Identifiers
urn:nbn:se:mdh:diva-21371 (URN)000335436800001 ()978-3-642-40561-7 (ISBN)978-3-642-40560-0 (ISBN)
Conference
11th International Conference on Software Engineering and Formal Methods, September 25-27. 2013, Madrid, Spain
Projects
ARROWS - Design Techniques for Adaptive Embedded Systems
Available from: 2013-09-17 Created: 2013-09-11 Last updated: 2015-11-13Bibliographically approved
7. Wind Turbine System: An Industrial Case Study in Formal Modeling and Verification
Open this publication in new window or tab >>Wind Turbine System: An Industrial Case Study in Formal Modeling and Verification
Show others...
2014 (English)In: Communications in Computer and Information Science, Volume 419 CCIS, 2014, 229-245 p.Conference paper, Published 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.

Keyword
Formal Modeling, Case Study
National Category
Electrical Engineering, Electronic Engineering, Information Engineering
Research subject
Computer Science
Identifiers
urn:nbn:se:mdh:diva-22326 (URN)10.1007/978-3-319-05416-2_15 (DOI)2-s2.0-84904627849 (Scopus ID)9783319054155 (ISBN)
Conference
2nd International Workshop of Formal Techniques for Safety-Critical Systems, FTSCS 2013; Queenstown; New Zealand; 29 October 2013 through 30 October 2013
Projects
ARROWS
Available from: 2013-11-01 Created: 2013-11-01 Last updated: 2015-02-05Bibliographically approved

Open Access in DiVA

fulltext(3649 kB)370 downloads
File information
File name FULLTEXT01.pdfFile size 3649 kBChecksum SHA-512
975cf0dbc44522459e1b9d6eea29b1362ccbd550095063e8ba435c6ac47d756d5e4741dc28f0a2299fc75a68e41f3b04eceed8a64bbed0692e3f737785323bc3
Type fulltextMimetype application/pdf

Search in DiVA

By author/editor
Suryadevara, Jagadish
By organisation
School of Innovation, Design and Engineering
Embedded Systems

Search outside of DiVA

GoogleGoogle Scholar
Total: 370 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

Total: 516 hits
CiteExportLink to record
Permanent link

Direct 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