Characterising for contemporary systems is their dependence on constituent systems to provide information, functionality, and scalability. Moreover, as the tasks that systems perform are ever more intimate and critical in their nature, reliability and correctness are great concerns. On these matters, we outline a methodology for formal integration of systems. We claim this formal approach to assist in managing the complexity and correctness, in preserving reliability and in respecting the independence of the constituent systems. As a proof of concept, we integrate two in-house control systems specified independently in the Event-B language with the Rodin Platform tool. Moreover, we show how to introduce a new functionality that is only possible due to the integration. Hence, we formally construct a system of systems and provide the methods for hierarchical integration of those. 1. Introduction Traditionally applications were developed to run on a certain hardware deployed in a specific environment in order to perform some tasks. This approach is still true for many modern deployments, especially those classified as critical systems having legislative regulations as a common nominator. Regulations on such systems are typically enforced by third-party actors. A third-party actor could be an authority supervising that extra-system interference is considered to an acceptable extent, for example, maintenance interval of the mass transport system’s platform screen doors or the calibration interval and tolerance of radars controlling the airspace. Commonly these regulated systems are monoliths; that is, even though the system may rely on constituent subsystems, all systems are modelled to completion. They are also the kind of implementations for which formal methods have been developed, of algorithmic nature. However, apart from critical systems and monolithic system design, the technological advances have enabled an abundance of deployment opportunities for computational devices. Applications relying on such systems provide a sense of comfort and ease our life making the supporting systems an integral part of our everyday lives. Prominent properties for such contemporary systems are their independence as well as their distributed nature. The independence properties are due to that such a system performs a task of its own regardless of its environment; for example, a weather forecast system forecasts the weather regardless how, if at all, this information is used. Distribution of systems is motivated by, among others, load balancing, optimization, and physical
References
[1]
J. Boardman and B. Sauser, “System of systems-the meaning of of,” in Proceedings of the 2006 IEEE/SMC International Conference on System of Systems Engineering, pp. 118–123, April 2006.
[2]
G. Banavar, J. Beck, E. Gluzberg, J. Munson, J. Sussman, and D. Zukowski, “Challenges: an application model for pervasive computing,” in Proceedings of the 6th Annual international Conference on Mobile Computing and Networking (MOBICOM '00), pp. 266–274, August 2000.
[3]
G. Banavar and A. Bernstein, “Software infrastructure and design challenges for ubiquitous computing applications,” Communications of the ACM, vol. 45, no. 12, pp. 92–96, 2002.
[4]
H. Zemanek, Abstract Architecture, General Concepts for Systems Design, Lecture Notes in Computer Science 86/1980, Winterschool on Abstract Software Specification at the Danish University of Technology, Copenhagen, Denmark, 1980.
[5]
P. Naur, “Formalization in program development,” BIT Numerical Mathematics, vol. 22, no. 4, pp. 437–453, 1982.
[6]
M. Shaw, “Beyond objects: a software design paradigm based on process control,” ACM SIGSOFT Software Engineering Notes, vol. 20, pp. 27–38, 1995.
[7]
M. Shaw and D. Garlan, Software Architecture, Mona Pompili, Prentice-Hall, New Jersey, NJ, USA, 1996.
[8]
G. Biegel and V. Cahill, “A framework for developing mobile, context-aware applications,” in Proceedings of the 2nd IEEE international Conference on Pervasive Computing and Communications (Percom '04), pp. 361–365, March 2004.
[9]
A. Fitzpatrick, G. Biegel, S. Clarke, and V. Cahill, “Towards a sentient object model,” in Proceedings of the Workshop on Engineering Context-Aware Object Oriented Systems and Environments (OOPSLA/ECOOSE '02), 2002.
[10]
J.-R. Abrial, Modeling in Event-B: System and Software Engineering, Cambridge University Press, New York, NY, USA, 2010.
[11]
S. Selberg and M. Austin, “Toward an evolutionary system of systems architecture,” in Proceedings of the 18th Annual International Symposium of The International Council on Systems Engineering (INCOSE '08), 2008.
[12]
R. J. R. Back and K. Sere, “Superposition refinement of reactive systems,” Formal Aspects of Computing, vol. 8, no. 3, pp. 324–346, 1996.
[13]
C. A. R. Hoare, “Communicating sequential processes,” Communications of the ACM, vol. 21, no. 8, pp. 666–677, 1978.
[14]
R. Milner, A Calculus of Communicating Systems, Springer, New York, NY, USA, 1980.
[15]
R. Milner, J. Parrow, and D. Walker, “A calculus of mobile processes, I,” Information and Computation, vol. 100, no. 1, pp. 1–40, 1992.
[16]
F. Arbab, “Reo: a channel-based coordination model for component composition,” Mathematical Structures in Computer Science, vol. 14, no. 3, pp. 329–366, 2004.
[17]
R. Back and R. Kurki-Suonio, “Decentralization of process nets with centralized control,” in Proceedings of the 2nd ACM SIGACT-SIGOPS Symposium on Principles of Distributed Computing, 1983.
[18]
J.-R. Abrial, The B-Book: Assigning programs to meanings, Cambridge University Press, New York, NY, USA, 1996.
[19]
J.-R. Abrial, M. Butler, S. Hallerstede, T. S. Hoang, F. Mehta, and L. Voisin, “Rodin: an open toolset for modelling and reasoning in Event-B,” International Journal on Software Tools for Technology Transfer, vol. 12, no. 6, pp. 447–466, 2010.
[20]
K. Mani Chandy, Parallel Program Design: A Foundation, Addison-Wesley Longman Publishing, Boston, Mass, USA, 1988.
[21]
C. Hoare, “An axiomatic basis for computer programming,” Communications of the ACM, vol. 12, no. 10, pp. 576–583, 1969.
[22]
E. W. Dijkstra, “Guarded commands, nondeterminacy and formal derivation of programs,” Communications of the ACM, vol. 18, no. 8, pp. 453–457, 1975.
[23]
A. Pnueli, “The temporal logic of programs,” in Proceedings of the 18th Annual Symposium on Foundations of Computer Science, pp. 46–57, 1977.
[24]
E. A. Emerson and J. Y. Halpern, “Decision procedures and expressiveness in the temporal logic of branching time,” Journal of Computer and System Sciences, vol. 30, no. 1, pp. 1–24, 1985.
[25]
M. W. Maier, “Architecting principles for system of systems,” Systems Engineering, vol. 1, no. 4, pp. 267–284, 1998.
[26]
A. Sage and S. Biemer, “Processes for system family architecting, design, and integration,” IEEE Systems Journal, vol. 1, no. 1, pp. 5–16, 2007.
[27]
A. Sage and C. Cuppan, “On the systems engineering and management of systems of systems and federations of systems,” Information Knowledge Systems Management, vol. 2, no. 4, pp. 325–345, 2001.
[28]
“Event-B and the Rodin Platform,” http://www.event-b.org/, 2013.
[29]
R. Back and K. Sere, “From action systems to modular systems,” in Proceedings of the 2nd International Symposium of Formal Methods Europe. Industrial Benefit of Formal Methods (FME '94), pp. 1–25, 1994.
“Decomposition Plug-in User Guide,” http://wiki.event-b.org/index.php/Decomposition_Plug-in_User_Guide, 2013.
[32]
J. R. Abrial, “Event Model Decomposition,” Wiki document Version 1. 3, http://wiki.event-b.org/images/Event_Model_Decomposition-1.3.pdf, 2009.
[33]
M. Butler, “Decomposition structures for event-B,” in Proceedings of the 7th International Conference on Integrated Formal Methods (IFM '09), 2009.
[34]
K. Sere, Stepwise derivation of parallel algorithms [Ph.D. thesis], ？bo Akademi, Department of Computer Science, Turku, Finland, 1990.
[35]
R. Back and K. Sere, “Stepwise refinement of action systems,” Structured Programming, vol. 12, no. 1, pp. 17–30, 1991.
[36]
S. Katz, “Superimposition control construct for distributed systems,” ACM Transactions on Programming Languages and Systems, vol. 15, no. 2, pp. 337–356, 1993.
[37]
C. Szypersk, Component Software, Addison-Wesley, Reading, Mass, USA, 1998.
[38]
C. Szyperski, D. Gruntz, and S. Murer, Component Software-Beyond Object-Oriented Programming-Second Edition, Addison-Wesley and ACM Press, Reading, Mass, USA, 2002.
[39]
T. Broens, Dynamic context bindings-Infrastructural support for context-aware applications [Ph.D. thesis], University of Twente, Enschede, The Netherlands, 2008, CTIT Ph.D.thesis series No. 08-125.
[40]
M. Wegdam, Dynamic reconfiguration and load distribution in component middleware [Ph.D. thesis], University of Twente, Enschede, The Netherlands, 2003.
[41]
M. Neovius, “Formal stepwise development of an in-house temperature control system,” TUCS Technical Reports 1078, 2013.
[42]
P. Sandvik, “Formal stepwise development of an in-house lighting control system,” TUCS Technical Reports 1079, 2013.
[43]
R. J. R. Back and J. von Wright, “Compositional action system refinement,” Formal Aspects of Computing, vol. 15, no. 2-3, pp. 103–117, 2003.
[44]
M. Neovius and K. Sere, “Formal modular modelling of context-awareness,” in Proceedings of the 7th International Symposium in Formal Methods for Components and Objects, Revised Lectures, pp. 102–118, 2008.
[45]
D. L. Parnas, “Really rethinking ‘formal methods’,” Computer, vol. 43, no. 1, Article ID 5398780, pp. 28–34, 2010.
[46]
H. Lieberman and T. Selker, “Out of context: computer systems that adapt to, and learn from, context,” IBM Systems Journal, vol. 39, no. 3-4, pp. 617–632, 2000.
[47]
R. Banach and M. Poppleton, “Sharp retrenchment, modulated refinement and simulation,” Formal Aspects of Computing, vol. 11, no. 5, pp. 498–540, 1999.
[48]
L. Lamport, “Temporal logic of actions,” ACM Transactions on Programming Languages and Systems, vol. 16, no. 3, pp. 872–923, 1994.
[49]
A. Iliasov, E. Troubitsyna, L. Laibinis, et al., “Supporting reuse in event B development: modularisation approach,” in Proceedings of Abstract State Machines, Alloy, B, and Z, (ABZ, 2010), pp. 174–188, 2010.
[50]
L. von Bertalanffy, General System Theory: Foundations, Development, Applications, Allen Lane, London, UK, 1971.
[51]
M. Neovius, Trustworthy context dependency in ubiquitous systems [Ph.D. thesis], ？bo Akademi University, Turku, Finland, 2012, TUCS Dissertations 151.
