Comparison of specification decomposition methods in Event-B


Citar

Texto integral

Acesso aberto Acesso aberto
Acesso é fechado Acesso está concedido
Acesso é fechado Somente assinantes

Resumo

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.

Sobre autores

P. Devyanin

Educational Information Security Community

Autor responsável pela correspondência
Email: peter_devyanin@hotmail.com
Rússia, Moscow

V. Kulyamin

Institute for System Programming; Moscow State University, Moscow, 119991 Russia GSP-1; National Research University Higher School of Economics

Email: peter_devyanin@hotmail.com
Rússia, ul. Solzhenitsyna 25, Moscow, 109004; Leninskie Gory, Moscow, 119991; 1-nd Kozhukhovsky proezd 1/7, Moscow, 101000

A. Petrenko

Institute for System Programming; Moscow State University, Moscow, 119991 Russia GSP-1; National Research University Higher School of Economics

Email: peter_devyanin@hotmail.com
Rússia, ul. Solzhenitsyna 25, Moscow, 109004; Leninskie Gory, Moscow, 119991; 1-nd Kozhukhovsky proezd 1/7, Moscow, 101000

A. Khoroshilov

Institute for System Programming; Moscow Institute of Physics and Technology

Email: peter_devyanin@hotmail.com
Rússia, ul. Solzhenitsyna 25, Moscow, 109004; Institutskii per. 9, Dolgoprudnyi, Moscow oblast, 141700

I. Shchepetkov

Institute for System Programming

Email: peter_devyanin@hotmail.com
Rússia, ul. Solzhenitsyna 25, Moscow, 109004

Arquivos suplementares

Arquivos suplementares
Ação
1. JATS XML

Declaração de direitos autorais © Pleiades Publishing, Ltd., 2016