20 citations · 25 across the 4 of their papers we have counts for
4 papers
Automating Verification of State Machines with Reactive Designs and Isabelle/UTP
Simon Foster, James Baxter, Ana Cavalcanti +2
State-machine based notations are ubiquitous in the description of component systems, particularly in the robotic domain. To ensure these systems are safe and predictable, formal v…
From Formalised State Machines to Implementations of Robotic Controllers
Wei Li, Alvaro Miyazawa, Pedro Ribeiro +3
Controllers for autonomous robotic systems can be specified using state machines. However, these are typically developed in an ad hoc manner without formal semantics, which makes i…
SCJ-Circus: a refinement-oriented formal notation for Safety-Critical Java
Alvaro Miyazawa, Ana Cavalcanti
Safety-Critical Java (SCJ) is a version of Java whose goal is to support the development of real-time, embedded, safety-critical software. In particular, SCJ supports certification…
Refinement-based verification of sequential implementations of Stateflow charts
Alvaro Miyazawa, Ana Cavalcanti
Simulink/Stateflow charts are widely used in industry for the specification of control systems, which are often safety-critical. This suggests a need for a formal treatment of such…