17 Result(s)
-
Chapter and Conference Paper
Refinement and Verification of Responsive Control Systems
Statechart notations with ‘run to completion’ semantics, are popular with engineers for designing controllers that respond to events in the environment with a sequence of state transitions. However, they lack ...
-
Chapter and Conference Paper
Formal Verification of Run-to-Completion Style Statecharts Using Event-B
Although popular in industry, state-chart notations with ‘run to completion’ semantics lack formal refinement and rigorous verification methods. State-chart models are typically used to design complex control ...
-
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
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
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 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 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...
-
Chapter and Conference Paper
A Generic Model for Assessing Process Quality
Process assessment and process improvement are both very difficult tasks since we are either assessing or improving a concept rather than an object. A quality process is expected to produce quality products ef...
