Abstract
The approach presented in this book relies on the unification of System specification environments for developing electronic Systems that are formally proven to be correct (correct-by-construction Systems). The key concept conveyed is the formal proof of System properties, which is carried out at every phase of the co-design cycle. The main idea is to build fully functional System modeis that are formally proven to be correct, and based on them to produce automatically the hardware and the Software parts of the System. The approach presented relies on the combined use of UML and B language.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
J-R. Abrial, The B Book: Assigning programs to meanings, Cambridge University Press, 1996.
J. Warmer, A. Kleppe, The Object Constraint Language: Precise Modeling with UML, Addison-Wesley, 1999.
P. Facon, R. Lelau, H.P. Nguyen, Combining UML with the B formal method for the Specification of database applications, Research Report, CEDRIC Laboratory, Paris, 1999.
ClearSy, Event B Reference Manual. Version 1.0, Available at: http://www.atelierb.societe.com/ressources/evt2b/eventb_reference_manual.pdf, 2001.
J. Draper et al, Evaluating the B method on an avionics example, Proceedings of Data Systems in Aerospace (DASIA) Conference, 1996.
C. Snook, L. Tsiopoulos, M. Waiden, A Case Study in Requirement Analysis ofControl Systems using UML and B, Proceedings of International Workshop on Refinement of Critical Systems, Methods, Tools and Developments, 2003.
J-R. Abrial, Event Driven Electronic Circuit Construction, Available at: http://www.atelierb.societe.com/ressources/articles/cir.pdf, 2001.
J-L. Boulanger et al, Formalization of Digital Circuits Using the B Method, Proceedings of 8th International Conference on Computer Aided Design, Manufacture and Operation in the Railway and Other Advanced Mass Transit Systems, 2002.
W. Ifill et al, The Use of B to Specify, Design and Verify Hardware, High Integrity Software, Springer Science+Business Media New York, 43–62, 2001.
PUSSEE Project. Available at: http://www.keesda.com/pussee, 2004.
KeesDA, BHDL User Guide. Preliminary Version, Available at http://www.keesda.com.
J-R. Abrial, Event Model Decomposition, Available at: http://www.atelierb.societe.com/resources/articles/dcmp3.pdf, 2001.
T. Lecomte, D4.4.1: Methodological Guidelines: Interface based synthesis/ refinement in B, IST-2000–30103 PUSSEE, Project Report, 2003.
T. Lecomte, J. R. Abrial, F. Badeau, C. Czernecki, D. Sabatier, C. Snook, Abstract modeling: System level modeiling and refinement in B, Technical Report, Project IST-2000–30103 PUSSEE, 2003.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer Science+Business Media New York
About this chapter
Cite this chapter
Voros, N.S., Snook, C., Hallerstede, S., Lecomte, T. (2004). Embedded System Design Using the PUSSEE Method. In: Mermet, J. (eds) UML-B Specification for Proven Embedded Systems Design. Springer, Boston, MA. https://doi.org/10.1007/978-1-4020-2867-0_3
Download citation
DOI: https://doi.org/10.1007/978-1-4020-2867-0_3
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-4419-5256-1
Online ISBN: 978-1-4020-2867-0
eBook Packages: Springer Book Archive