摘要
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.
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.
