KBN Research Project No 4 T11C 035 24
Applications of formal methods to support development of software for real-time systems
The research project is carried out by Computer Science Laboratory,
Department of Automatics,
AGH University of Science and Technology in Cracow, Poland.
The project deals with application of coloured Petri nets as a formal method for requirements specification of real-time systems, and as an algebraic and graphical language for design of executable models of such systems. Additionally, in accordance to properties analysis of developped systems, Petri nets will be supported by temporal logics and process algebras.
The main research objective is development of methods based on coloured Petri nets (including supporting formalisms) for development of correct software for real-time systems. Application of the formal methods will range from requierements specification to design phase.
Research results will be of theoretical sort, as well as will be confirmed by examples of practical applications.
It is expected to achieve the following research results.
An extension of applicability of D-nets by introducing hierarchization constructs and elaboration of
new methods for proving properties.
Development of methods and algorithms for formal analysis of requirements specification.
Development of methods for proving equivalences between coloured Petri net model and requirement specification.
Adaptation of bisimulation concept in the area of Petri nets and elaboration of the corresponding algorithms.
Adaptation of relative correctness concept and observation function for checking accordance between
Petri nets describing correspondingly requirement specification and the model.
Elaboration of verification methods for checking temporal properties in finite Petri net models.
A visible result of the project will be a CASE tool based on Petri nets formalism and devoted for
computer aided design of software for real-time systems. The tool will implement the current
results and the ones obtained during the project run. The software tool will be of standarised
input/output enabling cooperation with several existing systems for creation and analisis of Petri net models.