Incremental verification of architecture specification language for real-time systems

The concept of software architecture has recently emerged as a new way to improve our ability to effectively construct large scale software systems. However, there is no formal architecture specification language available to model and analyze complex real-time systems. In this paper, an object-oriented logic-based architecture specification language for real-time systems is discussed. Representation of real-time properties and timing constraints, and their integration with the language to model real-time concurrent systems is given. Architecture based specification languages enable the construction of large system architectures and provide a means of testing and validation. In general, checking the timing constraints of real-time systems is done by applying model checking to the constraint expressed as a formula in temporal logic. The complexity of such a formal method depends on the size of the representation of the system. A is possible that this size could increase exponentially when the system consists of several concurrently executing real-time processes. This means that the complexity of the algorithm will be exponential in the number of processes of the system and thus the size of the system becomes a limiting factor. Such a problem has been defined in literature as the ''state explosion problem''. We propose a method of incremental verification of architectural specifications for real-time systems. The method has a bower complexity in a sense that it does not work on the whole state space, but only on a subset of it that is relevant to the property to be verified.