onr:"swepub:oai:DiVA.org:ri-54339"
Search: onr:"swepub:oai:DiVA.org:ri-54339" > Towards a Verificat...
- 1 of 1
- Previous record
- Next record
- To hitlist
- Sirjani, MarjanMälardalens högskola,Inbyggda system,Reykjavik University, 101 Reykjavík, Iceland (author)
Towards a Verification-Driven Iterative Development of Software for Safety-Critical Cyber-Physical Systems
- Article/chapterEnglish2021
Publisher, publication year, extent ...
- 2021-05-24
- Springer Science and Business Media Deutschland GmbH,2021
- printrdacarrier
Numbers
- LIBRIS-ID:oai:DiVA.org:ri-54339
- https://urn.kb.se/resolve?urn=urn:nbn:se:ri:diva-54339URI
- https://doi.org/10.1186/s13174-021-00132-zDOI
- https://urn.kb.se/resolve?urn=urn:nbn:se:mdh:diva-54633URI
Supplementary language notes
- Language:English
- Summary in:English
Part of subdatabase
- SwePubSwePub
Classification
Notes
- Funding details: Stiftelsen för Strategisk Forskning, SSF; Funding details: VINNOVA; Funding details: Stiftelsen för Kunskaps- och Kompetensutveckling, KKS; Funding details: Mälardalens högskola, 111; Funding text 1: The research of the first three authors for this work is supported by the Serendipity project funded by the Swedish Foundation for Strategic Research (SSF). The research of the first two authors is also supported by the DPAC project funded by the Knowledge Foundation (KK-stiftelsen). The research of the first author is supported by the KKS SACSys project too. The research of the fourth and fifth authors is funded partially by Vinnova through the ITEA3 European TESTOMAT and XIVT [] projects. Open access funding provided by Mälardalen University.
- 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).
Subject headings and genre
- 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
- 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
Added entries (persons, corporate bodies, meetings, titles ...)
- Provenzano, LucianaMälardalen University, Sweden,Mälardalens universitet, Innovation och produktrealisering(Swepub:mdh)lpo01 (author)
- Abbaspour Asadollah, SaraMälardalens högskola,Inbyggda system(Swepub:mdh)sar02 (author)
- Helali Moghadam, MahshidMälardalens högskola,RISE,Industriella system,Mälardalen University, Sweden,Inbyggda system,RISE Research Institutes of Sweden, Västerås, Sweden(Swepub:mdh)mhi05 (author)
- Saadatmand, Mehrdad,1980-RISE,Industriella system,RISE Research Institutes of Sweden, Västerås, Sweden(Swepub:ri)MehrdadSaa@ri.se (author)
- Mälardalens högskolaInbyggda system (creator_code:org_t)
Related titles
- In:Journal of Internet Services and Applications: Springer Science and Business Media Deutschland GmbH12:11867-48281869-0238
Internet link
Find in a library
- Journal of Internet Services and Applications (Search for host publication in LIBRIS)
To the university's database
- 1 of 1
- Previous record
- Next record
- To hitlist
Find more in SwePub
- By the author/editor
- Sirjani, Marjan
- Provenzano, Luci ...
- Abbaspour Asadol ...
- Helali Moghadam, ...
- Saadatmand, Mehr ...
- About the subject
-
- NATURAL SCIENCES
- NATURAL SCIENCES
- and Computer and Inf ...
- and Computer Science ...
-
- NATURAL SCIENCES
- NATURAL SCIENCES
- and Computer and Inf ...
- Articles in the publication
- Journal of Inter ...
- By the university
- RISE
- Mälardalen University
Search outside SwePub
- Extend your search to:
- Google Book Search
- Google Scholar
Kungliga biblioteket hanterar dina personuppgifter i enlighet med EU:s dataskyddsförordning (2018), GDPR. Läs mer om hur det funkar här.
Så här hanterar KB dina uppgifter vid användning av denna tjänst.
- Copyright © LIBRIS - National Library Systems
- LIBRIS.kb.se
