WFRF:(Rodriguez Navas Guillermo)
Sökning: WFRF:(Rodriguez Navas Guillermo) > (2015-2019) > Bounded Invariance ...
Bounded Invariance Checking of Simulink Models
-
- Filipovikj, Predrag (författare)
- Mälardalens högskola,Inbyggda system
-
- Rodriguez-Navas, Guillermo (författare)
- Mälardalens högskola,Inbyggda system
-
- Seceleanu, Cristina, 1968- (författare)
- Mälardalens högskola,Inbyggda system
- (creator_code:org_t)
- 2019-04-08
- 2019
- Engelska.
- Ingår i: Proceedings of the ACM Symposium on Applied Computing. - New York, NY, USA : ACM. ; , s. 2168-2177
- Konferensbidrag (refereegranskat)
Abstract
Ämnesord
Stäng
- Currently, Simulink models can be verified rigorously against design errors or statistical properties. In this paper, we show how Simulink models can be formally analyzed against invariance properties using bounded model checking reduced to satisfiability modulo theories solving. In its basic form, the technique provides means for verification of an underlying model over bounded traces rigorously, however, in general the procedure is incomplete. We identify common Simulink block types and compositions by analyzing selected industrial models, and we show that for some of them the set of non-repeating states (reachability diameter) can be visited with a finite set of paths of finite length, yielding the verification complete. We complement our approach with a tool, called SyMC that automates the following: i) calculation of the reachability diameter size for some of the designs, ii) generation of finite (bounded) paths of the underlying Simulink model and their encoding into SMT-LIB format and iii) checking invariance properties using the Z3 SMT solver. To show the applicability of our approach, we apply it on a prototype implementation of an industrial Simulink model, namely Brake by Wire from Volvo Group Trucks Technology, Sweden.
Ämnesord
- TEKNIK OCH TEKNOLOGIER -- Elektroteknik och elektronik -- Datorsystem (hsv//swe)
- ENGINEERING AND TECHNOLOGY -- Electrical Engineering, Electronic Engineering, Information Engineering -- Computer Systems (hsv//eng)
Publikations- och innehållstyp
- ref (ämneskategori)
- kon (ämneskategori)
Till lärosätets databas
Hitta mer i SwePub
- Av författaren/redakt...
- Filipovikj, Pred ...
- Rodriguez-Navas, ...
- Seceleanu, Crist ...
- Om ämnet
-
- TEKNIK OCH TEKNOLOGIER
- TEKNIK OCH TEKNO ...
- och Elektroteknik oc ...
- och Datorsystem
- Artiklar i publikationen
- Proceedings of t ...
- Av lärosätet
- 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
