11 Result(s)
within
Colin Snook
Logics and Meanings of Programs
Mathematical Logic and Formal Languages
-
Chapter and Conference Paper
Refinement of Statecharts with Run-to-Completion Semantics
Statechart modelling notations, with so-called ‘run to completion’ semantics and simulation tools for validation, are popular with engineers for designing systems. However, they do not support formal refinemen...
-
Chapter and Conference Paper
Diagram-Led Formal Modelling Using iUML-B for Hybrid ERTMS Level 3
We demonstrate diagrammatic Event-B formal modelling of a hybrid, ‘fixed virtual block’ approach to train movement control for the emerging European Rail Traffic Management System (ERTMS) level 3. We perform a re...
-
Chapter and Conference Paper
Behaviour-Driven Formal Model Development
Formal systems modelling offers a rigorous system-level analysis resulting in a precise and reliable specification. However, some issues remain: Modellers need to understand the requirements in order to formul...
-
Chapter and Conference Paper
Analysing Security Protocols Using Refinement in iUML-B
We propose a general approach based on abstraction and refinement for constructing and analysing security protocols using formal specification and verification. We use class diagrams to specify conceptual syst...
-
Chapter and Conference Paper
Class-Diagrams for Abstract Data Types
We propose to extend iUML-B class-diagrams to elaborate Abstract Data Types (ADTs) specified using Event-B theories. Classes are linked to data types, while attributes and associations correspond to operators ...
-
Chapter and Conference Paper
Validating the Requirements and Design of a Hemodialysis Machine Using iUML-B, BMotion Studio, and Co-Simulation
We present a formal specification of a hemodialysis machine (HD machine) using Event-B. We model the HD machine using iUML-B state-machines and class diagrams and build a corresponding BMotion Studio visualisa...
-
Chapter and Conference Paper
On Component-Based Reuse for Event-B
Efficient reuse is a goal of many software engineering strategies and is useful in the safety-critical domain where formal development is required. Event-B can be used to develop safety-critical systems, but c...
-
Chapter and Conference Paper
Applying an Integrated Modelling Process to Run-time Management of Many-Core Systems
A Run-Time Management system for many-core architecture is aware of application requirements and able to save energy by sacrificing performance when it will have negligible impact on user experience. This paper o...
-
Chapter and Conference Paper
A Practical Approach for Closed Systems Formal Verification Using Event-B
Assurance of high integrity systems based on closed systems is a challenge that becomes difficult to overcome when a classical testing approach is used; in particular the evidence generated from a classical te...
-
Chapter and Conference Paper
UML-B: A Plug-in for the Event-B Tool Set
UML-B is a graphical formal modelling notation that relies on Event-B for its underlying semantics and is closely integrated with the ‘Rodin’, Event-B verification tools. UML-B is similar to UML but has its ow...
-
Chapter and Conference Paper
Refinement of Statemachines Using Event B Semantics
While refinement gives a formal underpinning to the development of dependable control systems, such models are difficult to communicate and reason about in a non-formal sense, particularly for validation by no...
