16 Result(s)
within
Colin Snook
Programming Languages, Compilers, Interpreters
Software Engineering
-
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
A Proposal of an Example and Experiments Repository to Foster Industrial Adoption of Formal Methods
Formal methods (in a broad sense) have been around almost since the beginning of computer science. Nonetheless, there is a perception in the formal methods community that take-up by industry is low considering...
-
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...
-
Article
A method of refinement in UML-B
UML-B is a ‘UML-like’ graphical front-end for Event-B that provides support for object-oriented and state machine modelling concepts, which are not available in Event-B. In particular, UML-B includes class dia...
-
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
Verification of UML Models by Translation to UML-B
UML-B is a ‘UML like’ notation based on the Event-B formalism which allows models to be progressively detailed through refinements that are proven to be consistent and to satisfy safety invariants using the Ro...
-
Chapter and Conference Paper
Refining Nodes and Edges of State Machines
State machines are hierarchical automata that are widely used to structure complex behavioural specifications. We develop two notions of refinement of state machines, node refinement and edge refinement. We co...
-
Chapter
Documenting the Progress of the System Development
While UML gives an intuitive image of the system, formal methods provide the proof of its correctness. We can benefit from both aspects by combining UML and formal methods. Even for the combined method we need...
-
Chapter and Conference Paper
Language and Tool Support for Class and State Machine Refinement in UML-B
UML-B is a ‘UML-like’ graphical front end for Event-B that provides support for object-oriented modelling concepts. In particular, UML-B supports class diagrams and state machines, concepts that are not explic...
-
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
Towards a Method for Rigorous Development of Generic Requirements Patterns
We present work in progress on a method for the engineering, validation and verification of generic requirements using domain engineering and formal methods. The need to develop a generic requirement set for s...
-
Chapter
Formal Development of Mechanisms for Tolerating Transient Faults
Transient faults belong to a wide-spread class of faults typical for control systems. These are the faults that only appear for a short period of time and might reappear later. However, even by appearing for a...
