6 Result(s)
within
Alvaro Miyazawa
Programming Languages, Compilers, Interpreters
Programming Techniques
-
Article
Open AccessProbabilistic modelling and verification using RoboChart and PRISM
RoboChart is a timed domain-specific language for robotics, distinctive in its support for automated verification by model checking and theorem proving. Since uncertainty is an essential part of robotic system...
-
Article
Open AccessRoboChart: modelling and verification of the functional behaviour of robotic applications
Robots are becoming ubiquitous: from vacuum cleaners to driverless cars, there is a wide variety of applications, many with potential safety hazards. The work presented in this paper proposes a set of construc...
-
Chapter and Conference Paper
Automating Verification of State Machines with Reactive Designs and Isabelle/UTP
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 verification techniques are im...
-
Article
An integrated semantics for reasoning about SysML design models using refinement
SysML is a variant of UML for systems design. Several formalisations of SysML (and UML) are available. Our work is distinctive in two ways: a semantics for refinement and for a representative collection of ele...
-
Chapter
Java in the Safety-Critical Domain
Safety-Critical Java (SCJ) is an Open Group standard that defines a novel version of Java suitable for programming systems with various levels of criticality. SCJ enables real-time programming and certificatio...
-
Chapter and Conference Paper
Formal Models of SysML Blocks
In this paper, we propose a formalisation of SysML blocks based on a state-rich process algebra that supports refinement, namely, CML. We first establish a set of guidelines of usage of SysML block definition ...
