Distribution Signals between the Transmitter and Antenna – Event B Model

What we have solved: the possibility to receive DVB-T (Digital Video Broadcasting Terrestrial) with respect to local conditions for signal. We have deduced: variables that represent a set of so-called useful signal, i.e. the signal suitable for further processing – amplification and distribution. As a case study we have choosed few examples using Event B Method to show possibilty of solving komplex projects by this method. The resulting program can be proven to be correct as for its theoretical backgrounds. It is based on Zermelo-Fraenkel set theory with axion of choice, the concept of generalized substitution and structuring mechanismus (machine, refinement, implementation). B methods are accompanied by mathematical proofs that justify them. Abstract machine in this example connected with mathematical modelling solves an ability to receive DVB-T signal from the plurality of signals, both useful and useless for further processing.

Vérification et validation formelles de systèmes interactifs fondées sur la preuve : application aux systèmes Multi-Modaux

This paper focuses on the formal validation and verification of multi-modal human computer interfaces. It describes part of the obtained results of the French RNRT VERBATIM project whose purpose is the Multimodal Interfaces BIformal Verification and Test Automation. This project focuses on the application of a formal technique, namely the event B method. This approach is based on a proof technique and therefore it does not suffer from the state number explosion problem occurring in classical model checking. We outline the capability of this technique to support the design of multi-modal human computer interfaces, in particular, the capability to support the expression and the verification of properties issued from the CARE family. The proposed approach uses notations and semi-formal techniques issued from the HCI design area. We apply our approach on a case study called "CLIPS Yellow Pages".

A Mechanically Proved and an Incremental Development of the Session Initiation Protocol INVITE Transaction

The Session Initiation Protocol (SIP) is an application layer signaling protocol used to create, manage, and terminate sessions in an IP based network. SIP is considered as a transactional protocol. There are two main SIP transactions, the INVITE transaction and the non-INVITE transaction. The SIP INVITE transaction specification is described in an informal way in Request for Comments (RFC) 3261 and modified in RFC 6026. In this paper we focus on the INVITE transaction of SIP, over reliable and unreliable transport mediums, which is used to initiate a session. In order to ensure the correctness of SIP, the INVITE transaction is modeled and verified using event-B method and its Rodin platform. The Event-B refinement concept allows an incremental development by defining the studied system at different levels of abstraction, and Rodin discharges almost all proof obligations at each level. This interaction between modeling and proving reduces the complexity and helps in assuring that the INVITE transaction SIP specification is correct, unambiguous, and easy to understand.

Formal Methods for Verifications of Reactive Systems

This chapter deals with the use of two verification approaches: theorem proving and model checking. The authors focus on the Event-B method by using its associated theorem proving tool (Click_n_Prove), and on the language TLA+ by using its model checker TLC. By considering the limitation of the Event-B method to invariance properties, the authors propose to apply the language TLA+ to verify liveness properties on a software behavior. The authors extend first the expressivity and the semantics of a B model (called temporal B model) to deal with the specification of fairness and eventuality properties. Second, they give transformation rules from a temporal B model into a TLA+ module. The authors present in particular, their prototype system called B2TLA+, that they have developed to support this transformation; then they can verify these properties thanks to the model checker TLC on finite state systems. For the verification of infinite-state systems, they propose the use of the predicate diagrams. The authors illustrate their approach on a case study of a parcel sorting system.