Refinement-oriented models of Stateflow charts

DOI10.1016/J.SCICO.2011.07.007zbMath1243.68152OpenAlexW2070528884MaRDI QIDQ436420

Ana Cavalcanti, Alvaro Miyazawa

Publication date: 20 July 2012

Published in: Science of Computer Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.scico.2011.07.007

zbMATH Keywords

verificationformal semanticstoolsSimulinkCircus

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (3)

Testing using CSP Models: Time, Inputs, and Outputs ⋮ Safety-critical Java programs from \textsf{Circus} models ⋮ Test selection for traces refinement

Uses Software

• Simulink
• StateFlow
• CZT
• ProofPower
• ClawZ
• LUSTRE
• Z
• Circus

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• From control law diagrams to Ada via \textsf{Circus}
• A refinement strategy for Circus
• Statecharts: a visual formalism for complex systems
• Type Checking Specifications
• Guarded commands, nondeterminacy and formal derivation of programs
• Modular code generation from synchronous block diagrams
• Unifying Theories in ProofPower-Z
• Fundamental Approaches to Software Engineering
• FM 2005: Formal Methods

This page was built for publication: Refinement-oriented models of Stateflow charts