Refinement and Validation of the Immune System Based on the Event-B Method

2019 ◽  
Author(s):  
Sheng-rong Zou ◽  
Li Chen ◽  
Chen Wang ◽  
Yu-dan Shu
Keyword(s):  
Immune System ◽  
B Method ◽  
Event B Method

Comparison of Event-B and B Method: Application in Immune System

2018 ◽  
pp. 317-326
Author(s):  
Sheng-rong Zou ◽  
Chen Wang ◽  
Si-ping Jiang ◽  
Li Chen
Keyword(s):  
Immune System ◽  
B Method

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

2014 ◽  
Vol 2014 ◽  
pp. 1-11
Author(s):  
Rajaa Filali ◽  
Mohamed Bouhdadi
Keyword(s):  
Session Initiation Protocol ◽  
Application Layer ◽  
Levels Of Abstraction ◽  
Signaling Protocol ◽  
Incremental Development ◽  
B Method ◽  
Almost All ◽  
Event B Method ◽  
Different Levels

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.

Event-B method and liveness properties

2010 ◽  
Vol 44 (9-10) ◽  
pp. 1119-1163
Author(s):  
Olfa Mosbahi ◽  
Jacques Jaray
Keyword(s):  
B Method ◽  
Liveness Properties ◽  
Event B Method

Encoding a process algebra using the Event B method

2009 ◽  
Vol 11 (3) ◽  
pp. 239-253 ◽  
Author(s):  
Yamine Ait-Ameur ◽  
Mickael Baron ◽  
Nadjet Kamel ◽  
Jean-Marc Mota
Keyword(s):  
Process Algebra ◽  
B Method ◽  
Event B Method

Formal Methods for Verifications of Reactive Systems

2011 ◽  
pp. 376-415
Author(s):  
Olfa Mosbahi ◽  
Mohamed Khalgui
Keyword(s):  
Theorem Proving ◽  
Reactive Systems ◽  
Prototype System ◽  
Model Checker ◽  
B Method ◽  
Liveness Properties ◽  
Finite State ◽  
Infinite State Systems ◽  
Sorting System ◽  
Event B Method

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.

Sign in / Sign up

Export Citation Format

Share Document