We gratefully acknowledge support from
the Simons Foundation and member institutions.
Full-text links:

Download:

Current browse context:

cs.SE

Change to browse by:

References & Citations

DBLP - CS Bibliography

Bookmark

(what is this?)
CiteULike logo BibSonomy logo Mendeley logo del.icio.us logo Digg logo Reddit logo ScienceWISE logo

Computer Science > Software Engineering

Title: Bounded Invariant Checking for Stateflow

Authors: Predrag Filipovikj (Scania CV AB), Gustav Ung (Scania CV AB), Dilian Gurov (KTH Royal Institute of Technology), Mattias Nyberg (Scania CV AB)
Abstract: 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.
Comments: In Proceedings FMAS2022 ASYDE2022, arXiv:2209.13181. arXiv admin note: substantial text overlap with arXiv:2103.06248
Subjects: Software Engineering (cs.SE); Formal Languages and Automata Theory (cs.FL)
Journal reference: EPTCS 371, 2022, pp. 38-52
DOI: 10.4204/EPTCS.371.3
Cite as: arXiv:2209.14028 [cs.SE]
  (or arXiv:2209.14028v1 [cs.SE] for this version)

Submission history

From: EPTCS [view email]
[v1] Wed, 28 Sep 2022 12:18:48 GMT (88kb)

Link back to: arXiv, form interface, contact.