Record:   Prev Next
Author Bernin, Fredrik
Title UML-B Specification for Proven Embedded Systems Design [electronic resource] / by Fredrik Bernin, Michael Butler, Dominique Cansell, Stefan Hallerstede, Klaus Kronlöf, Alexander Krupp, Thierry Lecomte, Michael Lundell, Ola Lundkvist, Michele Marchetti, Wolfgang Mueller, Ian Oliver, Denis Sabatier, Tim Schattkowsky, Colin Snook, Nikolaos S. Voros, Yann Zimmermann ; edited by Jean Mermet
Imprint Boston, MA : Springer US, 2004
book jacket
Descript 1 online resource (ix, 300 pages)
text txt rdacontent
computer c rdamedia
online resource cr rdacarrier
Note Preface -- Acknowledgements -- 1. An Introduction to Formal Methods -- 2. Formally Unified System Specification Environment with UML, B and SystemC -- 3. Embedded System Design Using the PUSSEE Method -- 4. System Level Modelling and Refinement with Event-B -- 5. The UML-B Profile for Formal Systems Modelling in UML -- 6. U2B -- 7. BHDL -- 8. Towards a Conceptual Framework for UML to Hardware Description Language Mappings -- 9. Interface-Based Synthesis Refinement in B -- 10. Refinement of Finite State Machines with Complementary Model Checking -- 11. Adaptive Cruise Control Case Study Design Experiment -- 12. Adaptive Cruise Controller Case Study -- 13. Formal Modelling of Electronic Circuits Using Event-B -- 14. The Echo Cancellation Unit Case Study -- 15. Results of the Mobile Design System Experiment -- 16. UML-B Specification and Hardware Implementation of a Hamming Coder/Decoder -- 17. The PUSSEE Method in Practice -- A1. Evaluation Criteria for Embedded System Design Methods
UML-B Specification for Proven Embedded Systems Design presents the perspective of the project on a Paradigm Unifying System Specification Environments for proven Electronic design (PUSSEE) as conceived in the course of the research during 2002 - 2003. The goal of the research in this project was to introduce the formal proof of system properties throughout a modular system design methodology that integrates sub-systems co-verification with system refinement and reusability of virtual system components. This is done by combining the formal and informal means of specification by way of the UML and B languages to allow the verification of system specifications through the composition of proven sub-systems (with some particular attention to interfaces, in line with the VSIA/SLIF approach). The link of B with C, VHDL and SystemC extends the correct-by-construction design process to lower system-on-chip (SoC) development stages. The production of proven embedded software is therefore complemented by the production of proven hardware. Prototype tools have been developed for the code generation from UML and B, and existing B verification tools will be extended to support IP reuse, according to the VSIA recommendations. The methodology and tools were validated through the development of three industrial applications: a wireless mobile terminal a telecom system-on-chip based on HIPERLAN/2 protocol and an anti-collision module for automobiles. The problem was known to be hard and the scope ambitious. But the seventeen chapters of UML-B Specification for Proven Embedded Systems Design, describing the main results obtained demonstrate the success of the research, acknowledged by the European reviewers. They are released to allow the largest audience including the various sectors of industry's system design engineers, university teachers and researchers. They will hopefully convince skeptical professionals that formal approaches can now cope with industrial strength problems
Link Print version: 9781441952561
Subject Engineering
Computer system performance
Engineering design
Computer engineering
Electronic books
Alt Author Butler, Michael
Cansell, Dominique
Hallerstede, Stefan
Kronlöf, Klaus
Krupp, Alexander
Lecomte, Thierry
Lundell, Michael
Lundkvist, Ola
Marchetti, Michele
Mueller, Wolfgang
Oliver, Ian
Sabatier, Denis
Schattkowsky, Tim
Snook, Colin
Voros, Nikolaos S
Zimmermann, Yann
Mermet, Jean
Record:   Prev Next