BE(Software Engineering)(Hons Class I)
Contact details for Ms Nisansala Yatapanage
Thesis
Verification of Large Scale System Specifications
Description
Software systems are becoming increasingly large and complex, and are often used in safety-critical applications. It is therefore essential to verify that the specifications of these systems are correct prior to building the system, to ensure it does not pose any safety risks. Model checking is an automated verification technique. However, model checking suffers from the state explosion problem, which prevents large systems from being verified. Slicing is a program analysis technique for eliminating sections of a program which are irrelevant, based on a given criterion. The aim of this project is to apply slicing techniques to specifications to reduce the size and complexity prior to the model checking stage. The specification language considered is the graphical Behavior Tree modelling language. The technique would allow more large systems to be verified at the specification stage.
Supervisors
Professor Abdul Sattar
Dr. Kirsten Winter (UQ)
Research expertise
- Software specification and verification
- Model checking
- Program slicing
- Failure Modes and Effects Analysis
- Modelling of complex systems
Publications
- Yatapanage, N., Winter, K. and S. Zafar. Slicing Behavior Tree Models for Verification. Theoretical Computer Science, IFIP Advances in Information and Comunication Technology. 323:125-139. 2010.
- Lindsay, P., Winter, K. and N. Yatapanage. Safety Assessment Using Behavior Trees and Model Checking, 8th IEEE International Conference on Software Engineering and Formal Methods (SEFM 2010), IEEE Computer Society. 2010.
- Grunske, L., Winter, K. and N. Yatapanage. Defining the Abstract Syntax of Visual Languages with Advanced Graph Grammars - A Case Study Based on Behavior Trees. Journal of Visual Languages and Computing, Elsevier. 19(3):343-379. 2008.
- Zafar, S., Colvin, R., Winter, K., Yatapanage, N. and G. Dromey. Early Validation and Verification of a Distributed Role-Based Access Control Model. Proceedings of the 14th Asia-Pacific Software Engineering Conference (APSEC2007), IEEE Computer Society. pp.430-437. 2007.
- Wen, L., Lin, K., Colvin, R., Seagrott, J., Yatapanage, N. and G. Dromey. “Integrare”- a Collaborative Environment for Behavior-Oriented Design. Cooperative Design, Visualization, and Engineering 4th International Conference CDVE2007. Proceedings, Lecture Notes in Computer Science. Springer-Verlag. 4674:122-131. 2007.
- Grunske, L., Lindsay, P., Yatapanage, N. and K. Winter. An Automated Failure Mode and Effect Analysis based on High-Level Design Specification with Behavior Trees. Integrated Formal Methods: 5th International Conference, IFM 2005. Proceedings. Lecture Notes in Computer Science. Springer-Verlag. 3771:129-149. 2005.
- So, H.B., Yatapanage, K.G., Yatapanage, N. and G. Sheridan. Minerosion3.01: a user friendly erosion monitoring and landscape design package. Australian Coal Association Research Programme Annual Conference, Emerald, June 2003.
- So, H.B., Yatapanage, K.G., Yatapanage, N. and G. Sheridan. Minerosion3.01: Public domain software package. http://www.uq.edu.au/soils/minerosion.htm. Oct 2003.