Modeling, analysis and verification of real-time software systems: an integrated approach

Abstract

Real-Time Systems (RTS) interact with their environment using time constrained input/output signals i.e. the systems process information and produce responses within a speci ed time otherwise failure of the systems may occur. The complexity of Real-Time Software Systems (RTSS) is continuously increasing which makes their design very challenging. Therefore, ensuring the correctness of such systems within the speci ed time constraints is a di cult and complex task. In this dissertation, we have presented some new ideas and developed some novel approaches for modeling, analysis and veri cation of RTSS through the di erent phases of development. We have considered some of the commonly used UML diagrams to develop our methodology. The model-driven approach is adequate to address the complex issues of RTSS. This enables the veri cation of design and potentially the automatic synthesis of implementations. We have developed a framework, which focuses on the modeling of real-time software development to capture di erent aspects of RTSS. We have introduced new user de ned data types with VSL and then addressed the representation of di erent UML diagrams by extending the MARTE metamodel. Software life cycle model consists of di erent interrelated stages, due to which, there is a requirement to verify inconsistencies among these stages. By checking consistency, we ensure that the properties of the di erent stages of a speci cation are consistent with each other and they do not oppose. The same holds for RTSS as well. In order to make our model more robust, we have developed a set of consistency rules within the design models and introduced formal approach for the automated veri cation of the consistency rules. A prime concern of RTSS is that all the requirements related to time must be traced in all the phases of software development life cycle consistently. We have developed a comprehensive framework for ensuring traceability of timing constraints from the requirements analysis phase into the design phase. This framework helps in veri cation of requirements in design, automatically generates the trace metrics based on UML diagrams, demonstrates the degree of coverage of timing requirements and nally features any missing requirements. In RTS, scheduling of tasks with hard deadlines has been an important area of research. The trouble of giving a guarantee of meeting hard deadlines of tasks lies in the issues of priority inversion and of deadlocks. To beat such di culties, a great resource access control protocol is required. To address this issue, we model, analyze and verify four existing protocols (Priority Inheritance Protocol, Priority Ceiling Protocol, Stack Based Priority Ceiling Protocol and Stack Based Preemption Ceiling Protocol) using UML/SPT based Sequence and Timing diagrams to study deadlock. We have focused on the occurrence of deadlock in the Priority Inheritance Protocol and prevention of this using other mentioned protocols. The methods and frameworks presented in this dissertation provide an integrated framework towards modeling, analysis and veri cation of RTSS.