kth.sePublications
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Bounded Invariant Checking for Stateflow
KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Theoretical Computer Science, TCS. Scania CV AB, Södertälje, Sweden.
Scania CV AB, Södertälje, Sweden.
KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Theoretical Computer Science, TCS.ORCID iD: 0000-0002-0074-8786
KTH, School of Industrial Engineering and Management (ITM), Engineering Design, Mechatronics and Embedded Control Systems. Scania CV AB, Södertälje, Sweden.ORCID iD: 0000-0001-6667-3783
2022 (English)In: Electronic Proceedings in Theoretical Computer Science, EPTCS, Open Publishing Association , 2022, p. 38-52Conference paper, Published paper (Refereed)
Abstract [en]

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. 

Place, publisher, year, edition, pages
Open Publishing Association , 2022. p. 38-52
Keywords [en]
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
National Category
Computer Sciences
Identifiers
URN: urn:nbn:se:kth:diva-328152DOI: 10.4204/EPTCS.371.3ISI: 001048896900006Scopus ID: 2-s2.0-85139852926OAI: oai:DiVA.org:kth-328152DiVA, id: diva2:1763560
Conference
4th International Workshop on Formal Methods for Autonomous Systems, FMAS 2022 and 4th International Workshop on Automated and Verifiable Software sYstem DEvelopment, ASYDE 2022, 26-27 September 2022
Note

QC 20230607

Available from: 2023-06-07 Created: 2023-06-07 Last updated: 2023-09-01Bibliographically approved

Open Access in DiVA

No full text in DiVA

Other links

Publisher's full textScopus

Authority records

Filipovikj, PredragGurov, DilianNyberg, Mattias

Search in DiVA

By author/editor
Filipovikj, PredragGurov, DilianNyberg, Mattias
By organisation
Theoretical Computer Science, TCSMechatronics and Embedded Control Systems
Computer Sciences

Search outside of DiVA

GoogleGoogle Scholar

doi
urn-nbn

Altmetric score

doi
urn-nbn
Total: 19 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf