onr:"swepub:oai:DiVA.org:ri-54339"
Sökning: onr:"swepub:oai:DiVA.org:ri-54339" > Towards a Verificat...
- 1 av 1
- Föregående post
- Nästa post
- Till träfflistan
- Sirjani, MarjanMälardalens högskola,Inbyggda system,Reykjavik University, 101 Reykjavík, Iceland (författare)
Towards a Verification-Driven Iterative Development of Software for Safety-Critical Cyber-Physical Systems
- Artikel/kapitelEngelska2021
Förlag, utgivningsår, omfång ...
- 2021-05-24
- Springer Science and Business Media Deutschland GmbH,2021
- printrdacarrier
Nummerbeteckningar
- 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
Kompletterande språkuppgifter
- Språk:engelska
- Sammanfattning på:engelska
Ingår i deldatabas
- SwePubSwePub
Klassifikation
Anmärkningar
- 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).
Ämnesord och genrebeteckningar
- 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
Biuppslag (personer, institutioner, konferenser, titlar ...)
- Provenzano, LucianaMälardalen University, Sweden,Mälardalens universitet, Innovation och produktrealisering(Swepub:mdh)lpo01 (författare)
- Abbaspour Asadollah, SaraMälardalens högskola,Inbyggda system(Swepub:mdh)sar02 (författare)
- 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 (författare)
- Saadatmand, Mehrdad,1980-RISE,Industriella system,RISE Research Institutes of Sweden, Västerås, Sweden(Swepub:ri)MehrdadSaa@ri.se (författare)
- Mälardalens högskolaInbyggda system (creator_code:org_t)
Sammanhörande titlar
- Ingår i:Journal of Internet Services and Applications: Springer Science and Business Media Deutschland GmbH12:11867-48281869-0238
Internetlänk
Hitta via bibliotek
- Journal of Internet Services and Applications (Sök värdpublikationen i LIBRIS)
Till lärosätets databas
- 1 av 1
- Föregående post
- Nästa post
- Till träfflistan
Hitta mer i SwePub
- Av författaren/redakt...
- Sirjani, Marjan
- Provenzano, Luci ...
- Abbaspour Asadol ...
- Helali Moghadam, ...
- Saadatmand, Mehr ...
- Om ämnet
-
- NATURVETENSKAP
- NATURVETENSKAP
- och Data och informa ...
- och Datavetenskap
-
- NATURVETENSKAP
- NATURVETENSKAP
- och Data och informa ...
- Artiklar i publikationen
- Journal of Inter ...
- Av lärosätet
- RISE
- Mälardalens universitet
Sök utanför SwePub
- Sök vidare i:
- 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 - Nationella bibliotekssystem
- LIBRIS.kb.se
