Conference proceedings article
Verification of Hybrid Controlled Processing ´Systems based on Decomposition and Deduction
Publication Details
Authors: | Frehse, G.; Stursberg, O.; Engell, S.; Huuck, R.; Lukoschus, B. |
Editor: | http://ieeexplore.ieee.org/ |
Publication year: | 2001 |
Pages range : | 150-155 |
Book title: | Intelligent Control, 2001. (ISIC '01). Proceedings of the 2001 IEEE International Symposium on |
ISBN: | 0-7803-6722-7 |
DOI-Link der Erstveröffentlichung: |
Abstract
While formal verification has been successfully used to analyze several academic examples of controlled hybrid systems, the application to real-world processing systems is largely restricted by the complexity of modeling and computation. This paper aims at improving the applicability by using decomposition and deduction techniques: A given system is first decomposed into a set of physical and/or functional units and modeled by communicating timed automata or linear hybrid automata. The so-called assumption/commitment method allows one to formulate requirements for the desired behavior of single modules or groups of modules. Model-checking is an appropriate technique to analyze whether the requirements (e.g. the exclusion of critical states) are fulfilled. By combining the analysis results obtained for single modules, properties of composed modules can be deduced. As illustrated for a laboratory plant, properties of the complete system for which direct model-checking is prohibitively expensive can be inferred by the iterative application of analysis and deduction
While formal verification has been successfully used to analyze several academic examples of controlled hybrid systems, the application to real-world processing systems is largely restricted by the complexity of modeling and computation. This paper aims at improving the applicability by using decomposition and deduction techniques: A given system is first decomposed into a set of physical and/or functional units and modeled by communicating timed automata or linear hybrid automata. The so-called assumption/commitment method allows one to formulate requirements for the desired behavior of single modules or groups of modules. Model-checking is an appropriate technique to analyze whether the requirements (e.g. the exclusion of critical states) are fulfilled. By combining the analysis results obtained for single modules, properties of composed modules can be deduced. As illustrated for a laboratory plant, properties of the complete system for which direct model-checking is prohibitively expensive can be inferred by the iterative application of analysis and deduction
