10 Result(s)
within
Chapter
Conference Paper
Colin Snook
Logics and Meanings of Programs
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
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
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
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...
