Comparison of specification decomposition methods in Event-B | Programming and Computer Software Skip to main content
Springer Nature Link
Log in

Comparison of specification decomposition methods in Event-B

  • Published:
Programming and Computer Software Aims and scope Submit manuscript

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.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
¥17,985 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price includes VAT (Japan)

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

Explore related subjects

Discover the latest articles, news and stories from top researchers in related subjects.

References

  1. Devyanin, P.N., Models of Security of Computer Systems: Access control and Data Flows, Moscow: Hot line Telecom, Moscow, 2013.

    Google Scholar 

  2. Devyanin, P.N., Security Conditions for Information Flows by Memory in the MROSL DP-model, Prikl. Diskr. Mat, Appendix, 2014, vol. 7, pp. 82–85.

    Google Scholar 

  3. Astra Linux. http://wwwastra-linuxcom

  4. Devyanin, P., Khoroshilov, A., Kuliamin, V., et al., Formal Verification of OS Security Model with Alloy and Event-B, Proc. of the Fourth Int. Conf. on Abstract State Machines, Alloy, B, TLA, VDM, and Z (ABZ- 2014), Toulouse 2014, pp. 309–313. https://wwwspringercom/us/book/9783662436516

    Google Scholar 

  5. Devyanin, P.N., Kulyamin V.V., Petrenko, A.K., et al., On the Representation of the MROSL DP-model in the Formalized Event-B Notation (Rodin Platform), Konf. RusKripto-2014 (Proc. of the Conf, RusKripto- 2014), Moscow, 2014. http://wwwruscryptoru/ resource/ summary/rc2014/05_devyaninpdf

    Google Scholar 

  6. Abrial, J.-R., Modeling in Event-B: System and Software Engineering, Cambridge: Cambridge University Press, 2010.

    Book  MATH  Google Scholar 

  7. Abrial, J.-R., M. Butler, S. Hallerstede, et al., Rodin: An Open Toolset for Modelling and Reasoning in Event-B, Int. J. on Software Tools for Technol. Transfer, 2010, vol. 12, no. 6, pp. 447–466.

    Article  Google Scholar 

  8. Kulyamin V.V., Methods of Software Verification, Competition of Reviews on Information and Telecommunication Systems, 2008.

    Google Scholar 

  9. Damchoom, K., An Incremental Refinement Approach to a Development of a Flash-Based File System in Event-B, Ph. D. thesis, University of Southampton, School of Electronics and Computer Science, 2010.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Educational Information Security Community, Moscow, Russia

    P. N. Devyanin

  2. Institute for System Programming, Russian Academy of Sciences, ul. Solzhenitsyna 25, Moscow, 109004, Russia

    V. V. Kulyamin, A. K. Petrenko, A. V. Khoroshilov & I. V. Shchepetkov

  3. Moscow State University, Moscow, 119991 Russia GSP-1, Leninskie Gory, Moscow, 119991, Russia

    V. V. Kulyamin & A. K. Petrenko

  4. National Research University Higher School of Economics, 1-nd Kozhukhovsky proezd 1/7, Moscow, 101000, Russia

    V. V. Kulyamin & A. K. Petrenko

  5. Moscow Institute of Physics and Technology, Institutskii per. 9, Dolgoprudnyi, Moscow oblast, 141700, Russia

    A. V. Khoroshilov

Authors
  1. P. N. Devyanin
    View author publications

    You can also search for this author inPubMed Google Scholar

  2. V. V. Kulyamin
    View author publications

    You can also search for this author inPubMed Google Scholar

  3. A. K. Petrenko
    View author publications

    You can also search for this author inPubMed Google Scholar

  4. A. V. Khoroshilov
    View author publications

    You can also search for this author inPubMed Google Scholar

  5. I. V. Shchepetkov
    View author publications

    You can also search for this author inPubMed Google Scholar

Corresponding author

Correspondence to P. N. Devyanin.

Additional information

Original Russian Text © P.N. Devyanin, V.V. Kulyamin, A.K. Petrenko, A.V. Khoroshilov, I.V. Shchepetkov, 2016, published in Programmirovanie, 2016, Vol. 42, No. 4.

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Devyanin, P.N., Kulyamin, V.V., Petrenko, A.K. et al. Comparison of specification decomposition methods in Event-B. Program Comput Soft 42, 198–205 (2016). https://doi.org/10.1134/S0361768816040022

Download citation

  • Received:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1134/S0361768816040022