C. Banphawatthanarak & B. H. Krogh (2000):
Verification of stateflow diagrams using smv: sf2smv 2.0.
Technical Report CMU-ECE-2000-020.
Carnegie Mellon University.
BS EN 61508-3:2002 (2002):
Functional safety of electrical/electronic/programmable electronic safety related systems – Part 1: General requirements.
P. Caspi et al. (2003):
From Simulink to SCADE/lustre to TTA: a layered approach for distributed embedded applications.
ACM SIGPLAN Notices 38(7),
pp. 153–162,
doi:10.1145/780753.780754.
A. L. C. Cavalcanti et al. (2011):
From control law diagrams to Ada via Circus.
FAC,
pp. 1–48,
doi:10.1007/s00165-010-0170-3.
A. L. C. Cavalcanti et al. (2003):
A Refinement Strategy for Circus.
FAC 15(2 - 3),
pp. 146–181,
doi:10.1007/s00165-003-0006-5.
C. Chen (2010):
Formal Analysis for Stateflow Diagrams.
In: SSIRI-C '10,
pp. 102–109,
doi:10.1109/SSIRI-C.2010.29.
E. W. Dijkstra (1975):
Guarded commands, nondeterminacy and formal derivation of programs.
Commun. ACM 18(8),
pp. 453–457,
doi:10.1145/360933.360975.
DO-178b (1992):
Software Considerations in Airborne Systems and Equipment Certification.
G. Hamon (2005):
A denotational semantics for Stateflow.
In: EMSOFT.
ACM,
pp. 164–172,
doi:10.1145/1086228.1086260.
G. Hamon & J. Rushby (2004):
An Operational Semantics for Stateflow.
In: FASE,
LCNS 2984.
Springer-Verlag,
Barcelona, Spain,
pp. 229–243,
doi:10.1007/s10009-007-0049-7.
D. Harel (1987):
Statecharts: A Visual Formalism for Complex Systems.
SCP 8(3),
pp. 231–274,
doi:10.1016/0167-6423(87)90035-9.
R. Lublinerman et al. (2009):
Modular code generation from synchronous block diagrams: modularity vs. code size.
In: POPL' 09.
ACM,
pp. 78–89,
doi:10.1145/1480881.1480893.
A. Miyazawa & A. L. C. Cavalcanti:
Refinement of the AbsoluteValue chart.
Available at www.cs.york.ac.uk/ alvarohm/refinement.
A. Miyazawa & A. L. C. Cavalcanti (2011):
A formal semantics of Stateflow charts.
Technical Report YCS-2011-461.
University of York.
A. Miyazawa & A. L. C. Cavalcanti (2011):
Refinement-oriented models of Stateflow charts.
SCP.
(to appear).
C. C. Morgan (1994):
Programming from Specifications.
Prentice Hall International Series in Computer Science.
E.-R. Olderog (1991):
Nets, terms and formulas: three views of concurrent processes and their relationship.
Cambridge University Press,
New York, NY, USA,
doi:10.1017/CBO9780511526589.
M. V. M. Oliveira (2006):
Formal Derivation of State-Rich Reactive Programs using Circus.
Department of Computer Science - University of York,
UK.
YCST-2006-02.
G. Reeve & S. Reeves (2006):
Logic and refinement for charts.
ACSC '06,
Australia,
pp. 13–23.
A. W. Roscoe (1998):
The Theory and Practice of Concurrency.
Prentice-Hall Series in Computer Science.
Prentice-Hall,
New York.
Oxford.
N. Scaife et al. (2004):
Defining and translating a "safe" subset of simulink/stateflow into lustre.
In: EMSOFT.
ACM,
pp. 259–268,
doi:10.1145/1017753.1017795.
The MathWorks,Inc.:
Real-Time Workshop.
www.mathworks.co.uk/products.
The MathWorks,Inc.:
Simulink.
www.mathworks.co.uk/products.
The MathWorks,Inc.:
Stateflow and Stateflow Coder 7 User's Guide.
www.mathworks.co.uk/products.
A. Tiwari (2002):
Formal semantics and analysis methods for Simulink Stateflow models.
Technical Report.
SRI International.
www.csl.sri.com/tiwari/stateflow.html.
A. Toom et al. (2008):
Gene-Auto: an Automatic Code Generator for a safe subset of Simulink/Stateflow and Scicos.
In: ERTS'08.
I. Toyn & A. Galloway (2005):
Proving properties of Stateflow models using ISO Standard Z and CADiZ.
In: ZB-2005, vol. 3455 of LNCS,
pp. 104–123,
doi:10.1007/11415787\voidb@x 0.06emwidth0.5em7.
J. C. P. Woodcock & A. L. C. Cavalcanti (2002):
The Semantics of Circus.
In: ZB 2002: Formal Specification and Development in Z and B,
LCNS 2272.
Springer-Verlag,
pp. 184–203,
doi:10.1007/3-540-45648-1\voidb@x 0.06emwidth0.5em10.
J. C. P. Woodcock & J. Davies (1996):
Using Z: specification, refinement, and proof.
Prentice-Hall, Inc..
eptcs@eptcs.org