The Infona portal uses cookies, i.e. strings of text saved by a browser on the user's device. The portal can access those files and use them to remember the user's data, such as their chosen settings (screen view, interface language, etc.), or their login data. By using the Infona portal the user accepts automatic saving and using this information for portal operation purposes. More information on the subject can be found in the Privacy Policy and Terms of Service. By closing this window the user confirms that they have read the information on cookie usage, and they accept the privacy policy and the way cookies are used by the portal. You can change the cookie settings in your browser.
This chapter begins with an introduction to the main concepts of formal methods. Languages and tools for developing formal System modeis are also described, while the use of semi formal notations and their integration with formal methods is covered as well. At the end of the chapter, an overview of the current Status of formal methods in embedded System design is presented.
A methodology for introducing formal proof to embedded Systems development. It is based on the formal semantics of B, uses UML notation as the primary design language, provides a formally provable decomposition techique, applies model checking for the verification of temporal properties and supports hardware synthesis in addition to Software implementation.
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...
Event B aims at providing a way to model Systems [1][2] that they are made of many parts interacting with a highly evolving (and sometimes hostile) environment. They also quite often involve several concurrent executing agents. They require a high degree of correctness. Finally, most of them are the result of a construction process which is spread over several years and which requires a large and...
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, are seen as difficult and costly to use and have achieved only limited use despite the benefits that they offer. In previous work, we have proposed an Integration of UML and the formal notation,...
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, are seen as difficult and costly to use and have achieved only limited use despite the benefits that they offer. In previous work, we have proposed an integration of UML and the formal notation,...
In this chapter we discuss modeling of hardware and translation to VHDL. Translation to SystemC or Verilog is similar. However VHDL is easier to read and we use VHDL synthesis tools. Translation is path complete path from formal models to a circuit. Equally important we need a refinement method to arrive at a formal circuit description that can be translated. This method has some significant differences...
In this chapter we discuss a conceptual framework for the basis of a UML profile for hardware/software co-design and the meta-models of the target languages such as SystemC used in this domain.
When specifying a system, the refinement process of the B method enables (inner part) and the interface (outer part) of a component, from its abstraction to its implementation, while verifying, by proof at each refinement step, that there is no contradiction between two successive refinement levels
We investigate a methodology for the refinement of finite state machines to time annotated finite state machines. We present a translation, which transforms models into B language code for efficient application of theorem proving. Refinement and verification is performed across three levels with the B-Method and with complementary verification through the RAVEN model checker. The presented methodology...
This chapter documents experience from a case study of adaptive cruise control (ACC). The chapter starts with a brief description of the model developed in the case study and an overview of the work performed in the case study. The main part of the chapter is organised in sections covering different aspects and issues encountered in the 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 Language are presented by the example of the case study.
This chapter presents cha resents a study of the SAE J1708 Serial Communication link described in [1]. The study is carried out in Event-B, an extension of the B method. The system is implemented and decomposed using step-wise refinement. We p resent how to derive with this method a cycle-accurate hardware model. The model of the communication link system is composed of an arbitrary, itra finite,...
This chapter describes a case study, which was performed in collaboration of Nokia Research and Paderborn University in the context of the methodology for refinement automation of finite state machines as presentedented in Chapter 10. We elaborate on a combined verification and refinement of an echo cancellation unit of a mobile phone with the Atelier-B toolkit and the RAVEN model checker. The experimental...
This case study involves the specification of a digital signal processor architecture as may be developed usingvelo ed usin MDA (Model Driven Architecture) techniques.
Formal refinement as offered by the B method has been shown to be applicable in practice and to scale up. However, it has been recognised that it is difficult communicate a formal B model with customers. Recently, as an interface to rigorous formal B models the UML has been investigated to facilitate this communication. The UML is generally accepted as being a communicating models of systems. Availability...
The main goal of this chapter is to demonstrate the feasibility of PUSSEE development framework. For that purpose, a case study borrowed from the telecommunication domain is used in order to exhibit the applicability the method and associated tools for the design of complex systems. The application described is part of an embedded system based on HIPERLAN/2 protocol.
This annex introduces a representative set of criteria for evaluating the applicability of system design methodologies in practice. The criteria cover a wide range of evaluation parameters, as they are perceived by system designers that apply system design methodologies in practice.
Set the date range to filter the displayed results. You can set a starting date, ending date or both. You can enter the dates manually or choose them from the calendar.