MENU
• Description
• News
• Staff
• Bibliography
• Links
• Adder Tools








       

AGH University of Science and Technology
Cracow, Poland
Department of Automatics
Computer Science Laboratory
Applications of formal methods
to support development of software for real-time systems

 

Saturday, 16 November 2024        
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.
  1. An extension of applicability of D-nets by introducing hierarchization constructs and elaboration of new methods for proving properties.
  2. Development of methods and algorithms for formal analysis of requirements specification.
  3. Development of methods for proving equivalences between coloured Petri net model and requirement specification.
  4. Adaptation of bisimulation concept in the area of Petri nets and elaboration of the corresponding algorithms.
  5. Adaptation of relative correctness concept and observation function for checking accordance between Petri nets describing correspondingly requirement specification and the model.
  6. 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.
E-mail: adder@agh.edu.pl