S. Nakajima (Japan)
Verification and Validation, Software Engineering, Real Time Software Architecture, Real-Time Maude, Data Con straints
Verification and validation of software architecture have been successful to use the state-space search methods such as the reachability analysis and the model-checking. The target system description to be analyzed is closed when conducting such state-space analyses. Although a cer tain abstraction technique is mandatory to reduce the state space size, the control aspects of the system external envi ronment and the data values input to the system are faith fully handled. This paper proposes to use the notion of data con straints for the specification and analysis of real-time sys tems written in Real-Time Maude. Since Real-Time Maude provides a systematic approach using the sampling abstrac tion method with the maximum time elapsed strategy, the analyses can be sound. Further, with the notion of data con straints, it is not necessary to provide all the possible data values while not sacrificing any of the interface information necessary for the analysis. The idea of integrating Real-Time Maude with the data constraints is useful for the analysis of real-time soft ware architecture in which timing constraint is a major con cern.
Important Links:
Go Back
