Comparison of specification decomposition methods in Event-B

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 reas...

Full description

Saved in:
Bibliographic Details
Published in:Programming and computer software 2016-07, Vol.42 (4), p.198-205
Main Authors: Devyanin, P. N., Kulyamin, V. V., Petrenko, A. K., Khoroshilov, A. V., Shchepetkov, I. V.
Format: Article
Language:English
Subjects:
Access control
Architecture (computers)
Artificial Intelligence
Complexity
Computer programs
Computer Science
Decomposition
Formal specification
Formal specifications
Information flow
Operating Systems
Programming
Software
Software Engineering
Software Engineering/Programming and Operating Systems
Specifications
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:0361-7688
1608-3261
DOI:10.1134/S0361768816040022