id:"swepub:oai:DiVA.org:kth-328152"
Search: id:"swepub:oai:DiVA.org:kth-328152" > Bounded Invariant C...
- 1 of 1
- Previous record
- Next record
- To hitlist
Bounded Invariant Checking for Stateflow
-
- Filipovikj, Predrag (author)
- KTH,Teoretisk datalogi, TCS,Scania CV AB, Södertälje, Sweden
-
- Ung, G. (author)
- Scania CV AB, Södertälje, Sweden
-
- Gurov, Dilian, 1964- (author)
- KTH,Teoretisk datalogi, TCS
- show more...
- show less...
- (creator_code:org_t)
- Open Publishing Association, 2022
- 2022
- English.
- In: Electronic Proceedings in Theoretical Computer Science, EPTCS. - : Open Publishing Association. ; , s. 38-52
- Conference paper (peer-reviewed)
Abstract
Subject headings
Close
- Stateflow models are complex software models, often used as part of industrial safety-critical software solutions designed with Matlab Simulink. Being part of safety-critical solutions, these models require the application of rigorous verification techniques for assuring their correctness. In this paper, we propose a refutation-based formal verification approach for analyzing Stateflow models against invariant properties, based on bounded model checking (BMC). The crux of our technique is: i) a representation of the state space of Stateflow models as a symbolic transition system (STS) over the symbolic configurations of the model, and ii) application of incremental BMC, to generate verification results after each unrolling of the next-state relation of the transition system. To this end, we develop a symbolic structural operational semantics (SSOS) for Stateflow, starting from an existing structural operational semantics (SOS), and show the preservation of invariant properties between the two. We define bounded invariant checking for STS over symbolic configurations as a satisfiability problem. We develop an automated procedure for generating the initial and next-state predicates of the STS, and a prototype implementation of the technique in the form of a tool utilising standard, off-the-shelf satisfiability solvers. Finally, we present preliminary performance results by applying our tool on an illustrative example and two industrial models.
Subject headings
- NATURVETENSKAP -- Data- och informationsvetenskap -- Datavetenskap (hsv//swe)
- NATURAL SCIENCES -- Computer and Information Sciences -- Computer Sciences (hsv//eng)
Keyword
- Computer programming languages
- Formal verification
- Model checking
- Semantics
- Simulink
- Bounded model checking
- Complex software
- Invariant checking
- Invariant properties
- Safety critical software
- Software modeling
- STATEFLOW
- Stateflow models
- Structural operational semantics
- Symbolic Transition Systems
- Accident prevention
Publication and Content Type
- ref (subject category)
- kon (subject category)
To the university's database
- 1 of 1
- Previous record
- Next record
- To hitlist
Find more in SwePub
- By the author/editor
- Filipovikj, Pred ...
- Ung, G.
- Gurov, Dilian, 1 ...
- Nyberg, Mattias
- About the subject
-
- NATURAL SCIENCES
- NATURAL SCIENCES
- and Computer and Inf ...
- and Computer Science ...
- Articles in the publication
- Electronic Proce ...
- By the university
- Royal Institute of Technology
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
