Page
%P
-
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...
-
Book
-
Chapter
Embedded System Design Using the PUSSEE Method
The approach presented in this book relies on the unification of System specification environments for develo** electronic Systems that are formally proven to be correct (correct-by-construction Systems). Th...
-
Chapter
The UML-B Profile for Formal Systems Modelling in UML
The UML is a populär modelling notation that has a natural appeal to hardware and Software engineers and is adaptable through extension mechanisms. Formal (mathematical) modelling languages, on the other hand,...
-
Chapter
The Adaptive Cruise Controller Case Study
We present the adaptive cruise controller case study for B modelling and the Abstract: We P data model checking by RAVEN. Individual translations of B operations, data types, and invariants to the RAVEN Input ...
-
Chapter
An Introduction to Formal Methods
This chapter begins with an introduction to the main concepts of formal methods. Languages and tools for develo** formal System modeis are also described, while the use of semi formal notations and their int...
-
Chapter
U2B
The UML is a popular modelling notation that has a natural appeal to hardware and software engineers and is adaptable through extension mechanisms. Formal (mathematical) modelling languages, on the other hand,...
-
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 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
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...
-
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
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
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
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
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...
-
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
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...
