Comparison of specification decomposition methods in Event-B |
| |
| Authors: | P. N. Devyanin V. V. Kulyamin A. K. Petrenko A. V. Khoroshilov I. V. Shchepetkov |
| |
| Affiliation: | 1.Educational Information Security Community,Moscow,Russia;2.Institute for System Programming,Russian Academy of Sciences,Moscow,Russia;3.Moscow State University, Moscow, 119991 Russia GSP-1,Leninskie Gory, Moscow,Russia;4.National Research University Higher School of Economics,Moscow,Russia;5.Moscow Institute of Physics and Technology,Dolgoprudnyi, Moscow oblast,Russia |
| |
| Abstract: | Decomposition is an important phase in the design of medium and large-scale systems. Various architectures of software systems and decomposition methods are studied in numerous publications. Presently, formal specifications of software systems are mainly used for experimental purposes; for this reason, their size and complexity are relatively low. As a result, in the development of a nontrivial specification, different approaches to the decomposition should be compared and the most suitable approach should be chosen. In this paper, the experience gained in the deductive verification of the formal specification of the mandatory entity-role model of access and information flows control in Linux (MROSL DP-model) using the formal Event-B method and stepwise refinement technique is analyzed. Two approaches to the refinementbased decomposition of specifications are compared and the sources and features of the complexity of the architecture of the model are investigated. |
| |
| Keywords: | |
| 本文献已被 SpringerLink 等数据库收录！ |
|
