Sökning: onr:"swepub:oai:DiVA.org:ri-54339" >
Towards a Verificat...
Towards a Verification-Driven Iterative Development of Software for Safety-Critical Cyber-Physical Systems
-
- Sirjani, Marjan (författare)
- Mälardalens högskola,Inbyggda system,Reykjavik University, 101 Reykjavík, Iceland
-
- Provenzano, Luciana (författare)
- Mälardalen University, Sweden,Mälardalens universitet, Innovation och produktrealisering
-
- Abbaspour Asadollah, Sara (författare)
- Mälardalens högskola,Inbyggda system
-
visa fler...
-
- Helali Moghadam, Mahshid (författare)
- Mälardalens högskola,RISE,Industriella system,Mälardalen University, Sweden,Inbyggda system,RISE Research Institutes of Sweden, Västerås, Sweden
-
- Saadatmand, Mehrdad, 1980- (författare)
- RISE,Industriella system,RISE Research Institutes of Sweden, Västerås, Sweden
-
visa färre...
-
(creator_code:org_t)
- 2021-05-24
- 2021
- Engelska.
-
Ingår i: Journal of Internet Services and Applications. - : Springer Science and Business Media Deutschland GmbH. - 1867-4828 .- 1869-0238. ; 12:1
- Relaterad länk:
-
https://doi.org/10.1...
-
visa fler...
-
https://jisajournal....
-
https://urn.kb.se/re...
-
https://doi.org/10.1...
-
https://urn.kb.se/re...
-
visa färre...
Abstract
Ämnesord
Stäng
- Software systems are complicated, and the scientific and engineering methodologies for software development are relatively young. Cyber-physical systems are now in every corner of our lives, and we need robust methods for handling the ever-increasing complexity of their software systems. Model-Driven Development is a promising approach to tackle the complexity of systems through the concept of abstraction, enabling analysis at earlier phases of development. In this paper, we propose a model-driven approach with a focus on guaranteeing safety using formal verification. Cyber-physical systems are distributed, concurrent, asynchronous and event-based reactive systems with timing constraints. The actor-based textual modeling language, Rebeca, with model checking support is used for formal verification. Starting from structured requirements and system architecture design the behavioral models, including Rebeca models, are built. Properties of interest are also derived from the structured requirements, and then model checking is used to formally verify the properties. This process can be performed in iterations until satisfaction of desired properties are ensured, and possible ambiguities and inconsistencies in requirements are resolved. The formally verified models can then be used to develop the executable code. The Rebeca models include the details of the signals and messages that are passed at the network level including the timing, and this facilitates the generation of executable code. The natural mappings among the models for requirements, the formal models, and the executable code improve the effectiveness and efficiency of the approach. © 2021, The Author(s).
Ämnesord
- NATURVETENSKAP -- Data- och informationsvetenskap -- Datavetenskap (hsv//swe)
- NATURAL SCIENCES -- Computer and Information Sciences -- Computer Sciences (hsv//eng)
- NATURVETENSKAP -- Data- och informationsvetenskap (hsv//swe)
- NATURAL SCIENCES -- Computer and Information Sciences (hsv//eng)
Nyckelord
- Cyber-physical systems
- Model checking
- Model driven development
- Requirements
- Safety-critical systems
- Verification & validation
- Complex networks
- Computer software
- Cyber Physical System
- Embedded systems
- Formal verification
- Iterative methods
- Modeling languages
- Safety engineering
- Software design
- Effectiveness and efficiencies
- Engineering methodology
- Executable codes
- Iterative development
- Model driven approach
- System architecture design
- Timing constraints
Publikations- och innehållstyp
- ref (ämneskategori)
- art (ämneskategori)
Hitta via bibliotek
Till lärosätets databas