Information Technology Reference
In-Depth Information
Building models of large and complex systems is not an easy task; the main
reason is that it can result in very complex models and dicult proofs. Apply-
ing this technique to the multi media system partly shows that the technique
can help overcome some of the complexity problems. Based on our experience
in this case study, we believe that atomicity decomposition can be scaled to
complex systems. The atomicity decomposition technique makes the standard
refinement more systematic and visual. Sequential relations between levels of
refinement during incremental modeling of a system are structured in atomicity
decomposition diagrams.
It is interesting to compare our approach to the media channel system with
the approach taken by Zave and Cheung [12]. Zave and Chueng present Promela
models of the behaviour of each end of the protocol (sender and initiator re-
spectively) and use the Spin model checker to verify that these models satisfy
certain safety and liveness properties. In our approach with Event-B, we start
with a more global view of the intension of the protocol and then use atomic-
ity decomposition to arrive at models that have similar levels of detail to the
Promela models since they include sending and receiving of messages by agents.
Sequential decomposition [7] appears to be a common pattern, but we illus-
trated two other patterns: the case splitting pattern and the guard line. Also we
believe that the graphical technique provides representing ways of other reusable
patterns. By modeling a wider range of systems on the future we anticipate the
discovery of more patterns. Providing a structured refinement guideline can be
considered as a future direction.
Atomicity decomposition provides a clear view of refinement steps, and can
help in constructing models. At this stage building Event-B models correspond-
ing to atomicity decomposition diagrams is done by hand, with some control
variables and guarded events. An automatic model builder from atomicity de-
composition diagrams will be developed in the future.
Acknowledgement
Partly supported by the EU research project ICT 214158 DEPLOY (Industrial
deployment of system engineering methods providing high dependability and
productivity) www.deploy-project.eu.
References
[1] Abrial, J.R.: Modeling in Event-B: System and Software Engineering. Cambridge
University Press, Cambridge (2010)
[2] Butler, M.: Incremental Design of Distributed Systems with Event-B. In: Mark-
toberdorf Summer School 2008 Lecture Notes. IoS (November 2008)
[3] de Willem Roever, P., Engelhardt, K.: Data Refinement: Model-oriented Proof
Theories and their Comparison Cambridge Tracts in Theoretical Computer Sci-
ence, vol. 46. Cambridge University Press, Cambridge (1998)
[4] Rezazadeh, A., Butler, M., Evans, N.: Redevelopment of an Industrial Case Study
Using Event-B and Rodin. In: BCS-FACS Christmas 2007 Meeting - Formal
Method. In: Industry (2007)
