Modeling in Event-B: System and Software Engineering B : Jean-Raymond Abrial 2011 20 9 1 1 1 2
3 4 5 6 6.2 6.3 7 7.1 7.2 7.3 7.4 7.5 7.6 7.7
22 1 1 (modeling) (formal reasoning) (before) (correct by construction) (practice in mind) (reason)
)
( ) Event-B
B
Event-B Action Systems [6]   TLA÷ [2]   VDM [15]    UNITY [5] ( ) Rodin Platform [7] ( event-b.org ) 1
2 2.1 1    : ) ( (modeling) (convention) (formal method) (requirement document) 2.2 2 : : (external observer) (correct) ( ) (correct by construction) (proof obligation rule) ×1 calculas) (basic arithmetic) (rules of inference of the sequent (propositional logic) (equality) : statement sentence .1 2.3 3 : 2 (design pattern) (invariant) (guard) 2.4 4 ) 2 ( 2 Lamport [2] 2 (universally quantified formula) 2.5 : Event-B 5 Event-B Event-B 14 2.6 6 : 4 (unreliable) (partially) 2 [8] 7 : 2.7 (distributed) (concurrent) (sequential) (15 (cooperate) ( 10, 11, 12, 13 4 6 (compete) ) (4-slot Fully Asynchronous mechanism) [14] 4 2.8 : 8 Event-B 15 2.9 9 : (transitive closure) (well-founded relations) (graph properties) ( (lists) (trees) ) 2.10 10    : 6 4 ( 2 (unique agent) G. Le Lann 70 ) ) ( 4 ) [9] (image of a set under a relation) (relational composition operator) (relational overriding operator) 2.11 11    : ( ) [10, 11] (induction rule) 9 2.12 12 .. 6 ( 13    : IEEE 1394 2.13 10 IEEE 1394 [13] ( (free tree) 9 2.14 14 : Event-B 5 (trace semantics) Event-B ) [12] : ) 2.15 . 15 (sequential composition) Event-B 2.16 16 : 2 （ 3  ） ) 2.17 . 17 (train system) (train agent) ( ) ( ( ) ) 2.18 .. 18 Rodin Rodin “event-b.org” ( ) ( ) Rodin 2.19 2 2 : ● 1 ● 2 ● 3 ) ● 4 ● 5 ) ● 9 ( ● 15 ( ) 2 ( ) Event-B 3 ( ) 4 ( ) ( ) ( 2 ) 5 (Event-B ) Event-B 9 ( ) 15 ( ) ( ) ( ) Rodin [7] Rodin 3 2 (sequential) (distributed) (concurrent) Event-B (parallel) DAG 11 ( ) 12 ( ） 13 (IEEE ） 17 ( ) Rodin [9] 3 (great confusion) : UML process) ( ) (program development : ( ) 1. 2. 3. (pseudo-programming) 4. 5. 4 : reason about their future system during its construction) (using an artifact to (blue-print) : (mock-up) : ( ) ( ) (building models) 5 (requirement document) 5.1 (activity)
(technical (very weak point) 5.2 (simple) (simply) (explanation) (requirement) 5.3 ( ) ( ) ( ) 1 1895 b ≤ a b ≈ c a c
a b ...口... ( ) 5.4 : 5.3 ( ) 2 (explanatory text) (reference text) 2 2 (labeled and numbered short statements) ) 2 : FUN:
(functional requirements) (environment requirements) (safety properties) (degraded mode requirements) (requirements concerned with delays)
(traceability) ( ) ( 6 model) (formal (classical logic) (pre-defined conventions) (set theory) (our model will thus not in general be executable) (complex) (discrete) 6.1 PC (system) (complex) 6.2 (discrete fashion) (abstract) (transition system) (a common point of departure) (one medium) 6.3 VS ( ) (correct) (laboratory execution) (lack of oracles) (beforehand) 2 （： ) (complex discrete system) (always postponing any serious thinking) ( ) confirmation) (routine (before) (proved reasoning) (discrete model) 7 3
(generic development) 7.1 (state) (event) condition)
(transition) (guard) (necessary 7.2 (operational interpretation) (operational semantics) (informal understanding) ( ) (no time) 2 . is said to have deadlocked) . (it (no assumption) 1 (not at all mandatory) 7.3 2 1 (invariant properties) (prove) (reachability) (modalities) 7.4 (closed model) 2 2 3 ) (refinement) (7.5 ） (generic instantiation) (7.7 ) (decomposition) (7.6 3 7.5 (gradually) (our look at it is only more accurate) (spatial extension) (temporal extension) (new events) (finer time granularity) 2 2 7.6 (data-refinement) 1 1 1 1 7.7 (carrier sets) 2 [1] J.R. Abrial. The B-book: Assigning Programs to Meanings. CUP 1996. [2] L. Lamport. Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley 1999. [3] F. Badeau. Using B as a high level programming language in an industrial project:  Roissy val. In Proceedings of ZB’ 05, 2005. [4] P. Behm. Meteor: A successful application of B in a large project. In Proceedings of FM   99, 1999. [5] K.M. Chandy and J. Misra. Parallel Program Design, a Foundation. Addison-Wesley, 1988. [6] R.J. Back and R. Kurki-Suonio. Distributed Cooperation with Action Systems. ACM Transaction on Program-ming Languages and Systems. 10(4): 513-554, 1988. [7] Rodin. European Project Rodin. http://rodin.cs.ncl.ac.uk. [8] J.F. Groote and J.C. Van de Pol A bounded retransmission protocol for large data packets - a case study in computer checked algebraic verification. Algebraic Methodology and Software Technology, 5th International Conference AMAST ' 96, Munich. Lecture Notes in Computer Science 1101. [9] G. Le Lann. Distributed systems - towards a formal approach. In B Gilchrist, editor Information Processing 77 North-Holland 1977. [10] N. Lynch. Distributed Algorithms. Morgan Kaufmann Publishers 1996. [11] W.H.J. Feijen and A.J.M. van Gasteren. On a Method of Multi-programming Springer 1999. [12] L. Moreau. Distributed Directory Service and Message Routers for Mobile Agent. Science of Computer Programming 39(2-3):249-272, 2001. [13] IEEE Standard for a High Performance Serial Bus. Std 1394-1995, August 1995. [14]  H.R. Simpson. Four-slot Fully Asynchronous Communication Mechanism. Computer and Digital Techniques. IEE Proceedings. Vol 137 (1) (Jan 1990). [15] C.B. Jones. Systematic Software Development using VDM. Prentice Hall International (1990).