Abstract

Modern systems tend to exhibit an ever increasing complexity especially due to their software design components and programmable aspects which are nowadays ubiquitous. Consequently, in order to assure reliable and dependable systems, sustained efforts are required in the process of system verification and validation. However, conventional verification and validation techniques that are primarily based on testing and simulation, while being helpful and useful, may lack in many cases the desired level of rigor and completeness and are generally costly, laborious and time consuming. In contrast, using verification techniques that are based on formal foundations, such as model-checking and program analysis in a complementary manner to the traditional verification techniques can provide an increased level of reliability and dependability. In this context, applying such techniques for verifying the correctness and validity of the engineered systems early in the design phase can greatly improve the quality and performance of the design. Moreover, using such a verification methodology can alleviate the high cost of maintaining the systems later in their development phases. Presently, modern system design can benefit from a wide range of development paradigms including those that are using techniques traditionally employed in software engineering such as the object oriented design paradigm. In order to standardize the process of system design and development, several modeling languages emerged in order to provide the means for capturing and modeling various system specifications and requirements. The Unified Modeling Language (UML) 2.0 and more recently the Systems Modeling Languages (SysML) represent the most prominent standardized modeling languages for software and systems engineering. In this setting, the research initiative that this work addresses, is introducing a unified paradigm for the verification and validation of software intensive systems engineering design models by using formal verification techniques that can be applied in order to assess different behavioral diagrams belonging to the aforementioned modeling languages.