-
Article
Open AccessFormal design, verification and implementation of robotic controller software via RoboChart and RoboTool
Current practice in simulation and implementation of robot controllers is usually undertaken with guidance from high-level design diagrams and pseudocode. Thus, no rigorous connection between the design and th...
-
Chapter
Model-Based Engineering for Robotics with RoboChart and RoboTool
Use of simulation to support the design of software for robotic systems is pervasive. Typically, roboticists draw a state machine using an informal notation (not precise or machine checkable) to convey a desig...
-
Chapter
Bringing RoboStar and RT-Tester Together
In recent work, Cavalcanti and her group, including Miyazawa and Timmis, have developed a CSP-based framework for model-based engineering of robotic systems, called RoboStar. In this paper, we describe our cur...
-
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...
-
Chapter
RoboStar Technology: A Roboticist’s Toolbox for Combined Proof, Simulation, and Testing
Simulation is favored by roboticists to evaluate controller design and software. Often, state machines are drawn to convey overall ideas and used as a basis to program tool-specific simulations. The simulation...
-
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
From Formalised State Machines to Implementations of Robotic Controllers
for robotic can using state . However, these are typically developed in an ad hoc manner without formal semantics, which makes it difficult to analyse the controller. Simulations are often used during...
-
Chapter and Conference Paper
Modelling and Verification for Swarm Robotics
RoboChart is a graphical domain-specific language, based on UML, but tailored for the modelling and verification of single robot systems. In this paper, we introduce RoboChart facilities for modelling and veri...
-
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
Sound Simulation and Co-simulation for Robotics
Software engineering for modern robot applications needs attention; current practice suffers from costly iterations of trial and error, with hardware and environment in the loop. We propose the adoption of an ...
-
Chapter and Conference Paper
Modelling and Verification of Timed Robotic Controllers
Designing robotic systems can be very challenging, yet controllers are often specified using informal notations with development driven primarily by simulations and physical experiments, without relation to ab...
-
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
Refinement Strategies for Safety-Critical Java
Safety-Critical Java (SCJ) is a version of Java that supports the development of real-time, embedded, safety-critical software. SCJ introduces abstractions that enforce a simpler architecture, and simpler conc...
-
Article
Refinement-based verification of implementations of Stateflow charts
Simulink’s Stateflow is a graphical notation widely adopted in industry. Since it is frequently used to model safety-critical systems, correctness of implementations of Stateflow charts is a major concern. In ...
-
Chapter and Conference Paper
Assurance Cases for Block-Configurable Software
One means of supporting software evolution is to adopt an architecture where the function of the software is defined through reconfiguring the flow of execution and parameters of pre-existing components. For s...
-
Chapter and Conference Paper
Formal Refinement in SysML
SysML is a UML-based graphical notation for systems engineering that is becoming a de facto standard. Whilst it reuses a number of UML diagrams, it introduces new diagrams, and maintains the loose UML semantics. ...
-
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 ...
