LTS Semantics Model of Event-B Synchronization Control Flow Design Patterns
0
조회
0
다운로드
1
인용
0
참고문헌
키워드
초록
The Event-B design pattern is an excellent way to quickly develop a formal model of the system. Researchershave proposed a number of Event-B design patterns, but they all lack formal behavior semantics. This makesthe analysis, verification, and simulation of the behavior of the Event-B model very difficult, especially for thecontrol-intensive systems. In this paper, we propose a novel method to transform the Event-B synchronouscontrol flow design pattern into the labeled transition system (LTS) behavior model. Then we map the designpattern instantiation process of Event-B to the instantiation process of LTS model and get the LTS behaviorsemantic model of Event-B model of a multi-level complex control system. Finally, we verify the linear temporallogic behavior properties of the LTS model. The experimental results show that the analysis and simulation ofsystem behavior become easier and the verification of the behavior properties of the system become convenientafter the Event-B model is converted to the LTS model.
Abstract
The Event-B design pattern is an excellent way to quickly develop a formal model of the system. Researchershave proposed a number of Event-B design patterns, but they all lack formal behavior semantics. This makesthe analysis, verification, and simulation of the behavior of the Event-B model very difficult, especially for thecontrol-intensive systems. In this paper, we propose a novel method to transform the Event-B synchronouscontrol flow design pattern into the labeled transition system (LTS) behavior model. Then we map the designpattern instantiation process of Event-B to the instantiation process of LTS model and get the LTS behaviorsemantic model of Event-B model of a multi-level complex control system. Finally, we verify the linear temporallogic behavior properties of the LTS model. The experimental results show that the analysis and simulation ofsystem behavior become easier and the verification of the behavior properties of the system become convenientafter the Event-B model is converted to the LTS model.
참고문헌 (25)
- J. R. Abrial, "Modeling in Event-B: System and Software Engineering" (2010), Cambridge University Press
- T. S. Hoang, "Event-B patterns and their tool support", Software & Systems Modeling, 12(2), pp.229~244 (2013)
- I. Tounsi, "Towards an approach for modeling and formalizing soa design patterns with Event-B", Proceedings of the 28th Annual ACM Symposium on Applied Computing, pp.1937~1938 (2013)
- A. Gondal, "Software Composition", pp.100~115 (2011), Springer
- A. Gondal, "Feature-oriented reuse with Event-B and Rodin", Ph.D., pp.2013
- A. Intana, "Formal engineering methodologies for wireless sensor network development with simulation", Ph.D., pp.2015
- "Application of decomposition and generic instantiation" (2011)[URL]
- R. Silva, "Formal Methods and Software Engineering", pp.466~484 (2009), Springer
- S. Yeganefard, "Evaluation of a guideline by formal modelling of cruise control system in Event-B", Proceedings of the Second NASA Formal Methods Symposium (NFM 2010), pp.182~191 (2010)
- S. Yeganefard, "Problem decomposition and sub-model reconciliation of control systems in Event-B", Proceedings of 2013 IEEE 14th International Conference on Information Reuse & Integration (IRI), pp.528~535 (2013)
- S. Yeganefard, "Structuring functional requirements of control systems to facilitate refinementbased formalisation", Electronic Communications of the EASST, 46, pp.1~15 (2011)
- S. Yeganefard, "Control systems: phenomena and structuring functional requirement documents", Proceedings of 2012 IEEE 17th International Conference on Engineering of Complex Computer Systems, pp.39~48 (2012)
- A. S. Fathabadi, "Software Engineering and Formal Methods", pp.78~93 (2012), Springer
- E. Alkhammash, "Building traceable Event-B models from requirements", Science of Computer Programming, 111, pp.318~338 (2015)
- A. S. Fathabadi, "Formal Methods for Components and Objects", pp.89~104 (2009), Springer
- A. S. Fathabadi, "NASA Formal Methods", pp.328~342 (2011), Springer
- A. Iliasov, "Software Engineering for Resilient Systems", pp.9~23 (2011), Springer
- S. Schneider, "Integrated Formal Methods", pp.260~274 (2010), Springer
- S. Schneider, "Bounded retransmission in Event-B∥CSP : a case study", Electronic Notes in Theoretical Computer Science, 280, pp.69~80 (2011)
- Stepwise refinement in Event-B CSP. Part 1: Safety, "S. Schneider", Department of Computing, University of Surrey, ~ (2011)
- S. Schneider, "The behavioural semantics of Event-B refinement", Formal Aspects of Computing, 26(2), pp.251~280 (2014)
- S. Schneider, "Integrated Formal Methods", pp.221~237 (2014), Springer
- T. S. Hoang, "Foundations for using linear temporal logic in Event-B refinement", Formal Aspects of Computing, 28(6), pp.909~935 (2016)
- R. Gorrieri, "Process Algebras for Petri Nets", pp.15~34 (2017), Springer
- K. G. Larsen, "UPPAAL in a nutshell", International Journal on Software Tools for Technology Transfer(STTT), 1(1), pp.134~152 (1997)