A Study on Configuration and Integration of Sub-Systems to System-of-Systems with Rule Verification

Tim Warnecke

Department of Computer Science, TU Clausthal, Clausthal-Zellerfeld, Germany.

DOI: 10.4236/eng.2015.710056                

Abstract

Increasing complexity of today’s software systems is one of the major challenges software engineers have to face. This is aggravated by the fact that formerly isolated systems have to be interconnected to more complex systems, called System-of-Systems (SoS). Those systems are in charge to provide more functionality to the user than all of their independent sub-systems could do. Reducing the complexity of such systems is one goal of the software engineering paradigm called component-based software engineering (CBSE). CBSE enables the developers to treat individual sub-systems as components which interact via interfaces with a simulated environment. Thus those components can be developed and implemented independently from other components. After the implementation a system integrator is able to interconnect the components to a SoS. Despite this much-used approach it is possible to show that constraints, which are valid in an isolated sub-system, are broken after this system is integrated into a SoS. To emphasize this issue we developed a technique based on interconnected timed automata for modelling sub-systems and System-of-Systems in the model checking tool UPPAAL. The presented modelling technique allows it to verify the correctness of single sub-systems as well as the resulting SoS. Additionally we developed a tool which abstracts the complicated timed automata to an easy to read component based language with the goal to help system integrators building and verifying complex SoS.

Keywords

System-of-Systems, CBSE, Verification, Model Checking, UPPAAL

Conflicts of Interest

The authors declare no conflicts of interest.

References

[1]	Szyperski, C. (2002) Component Software: Beyond Object-Oriented Programming. Addison-Wesley Longman Publishing Co., Inc., Boston.
[2]	Larsen, K.G., Pettersson, P. and Yi, W. (1997) Uppaal in a Nutshell. International Journal on Software Tools for Technology Transfer, 1, 134-152. http://dx.doi.org/10.1007/s100090050010
[3]	Clarke, E.M. and Emerson, E.A. (1982) Design and Synthesis of Synchronization Skeletons Using Branching Time Temporal Logic. In: Kozen, D., Ed., Logics of Programs, Springer Berlin Heidelberg, 52-71. http://dx.doi.org/10.1007/bfb0025774
[4]	Kripke, S.A. (1963) Semantical Considerations on Modal Logic. Acta Philosophica Fennica, 16, 83-94.
[5]	Owicki, S. and Lamport, L. (1982) Proving Liveness Properties of Concurrent Programs. ACM Transactions on Programming Languages and Systems, 4, 455-495. http://dx.doi.org/10.1145/357172.357178
[6]	Kuhn, S.J. (1980) Modal Logic: An Introduction. xii, 295. In: Chellas, B.F., Ed, Dialogue: Canadian Philosophical Review/Revue Canadienne de Philosophie, Vol. 21, Cambridge University Press, New York, 545-549.
[7]	Emerson, E.A. and Halpern, J.Y. (1986) “Sometimes” and “Not Never” Revisited: On Branching versus Linear Time Temporal Logic. Journal of the ACM, 33, 151-178. http://dx.doi.org/10.1145/4904.4999
[8]	Clarke, E.M. (2008) The Birth of Model Checking. In: Grumberg, O. and Veith, H., Eds., 25 Years of Model Checking, Springer Berlin Heidelberg, 1-26. http://dx.doi.org/10.1007/978-3-540-69850-0_1
[9]	Clarke, E.M., Klieber, W., Novácek, M. and Zuliani, P. (2012) Model Checking and the State Explosion Problem. In: Meyer, B. and Nordio, M., Eds., Tools for Practical Software Verification, Springer Berlin Heidelberg, 1-30. http://dx.doi.org/10.1007/978-3-642-35746-6_1
[10]	McMillan, K.L. (1993) Symbolic Model Checking. Symbolic Model Checking. Springer, 25-60. http://dx.doi.org/10.1007/978-1-4615-3190-6_3
[11]	Godefroid, P. and Wolper, P. (1992) Using Partial Orders for the Efficient Verification of Deadlock Freedom and Safety Properties. In: Larsen K.G. and Skou, A., Eds., Computer Aided Verification, Springer Berlin Heidelberg, 332-342. http://dx.doi.org/10.1007/3-540-55179-4_32
[12]	Clarke, E., Grumberg, O., Jha, S., Lu, Y. and Veith, H. (2000) Counterexample-Guided Abstraction Refinement. In: Emerson, E.A. and Sistla, A.P., Eds., Computer Aided Verification, Springer Berlin Heidelberg, 154-169. http://dx.doi.org/10.1007/10722167_15
[13]	Uppsala University, Aalborg University UPPAAL. www.uppaal.org