Using PVS to analyze hierarchical state-based requirements for completeness and consistency Export

@proceedings{heimdahl1997usingpvs, abstract = {Previously, we have defined procedures for analyzing hierarchical state based requirements specifications for two properties: (1) completeness with respect to a set of criteria related to robustness (a response is specified for every possible input and input sequence) and (2) consistency (the specification is free from conflicting requirements and undesired nondeterminism) (M.P.E. Heimdahl and N.G. Leveson, 1995; 1996). We implemented the analysis procedures in a prototype tool and evaluated their effectiveness and efficiency on a large real world requirements specification expressed in an hierarchical state based language called RSML (Requirements State Machine Language). Although our approach has been largely successful, there are some drawbacks with the current implementation that must be addressed. Our prototype implementation uses Binary Decision Diagrams (BDDs) to perform the analysis. Unfortunately, since BDDs treat predicates and functions as uninterpreted and thus fail to capture their semantics, the use of BDDs can lead to large numbers of spurious (false) error reports. We are currently investigating how the Prototype Verification System (PVS) and its theorem proving component can help us increase the accuracy of our analysis. PVS is a verification system that provides an interactive environment for writing formal specifications and checking formal proofs. The paper discusses the problems with spurious error reports and describes our experiences using the Prototype Verification System to increase the accuracy of our analysis results}, author = {Heimdahl, M. P. E. and Czerny, B. J.}, citeulike-article-id = {5784951}, citeulike-linkout-0 = {http://dx.doi.org/10.1109/HASE.1996.618606}, citeulike-linkout-1 = {http://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber=618606}, day = {06}, doi = {10.1109/HASE.1996.618606}, journal = {High-Assurance Systems Engineering Workshop, 1996. Proceedings., IEEE}, keywords = {requirements}, month = {August}, pages = {252--262}, posted-at = {2009-09-15 03:44:59}, priority = {3}, title = {Using PVS to analyze hierarchical state-based requirements for completeness and consistency}, url = {http://dx.doi.org/10.1109/HASE.1996.618606}, year = {2002} }

TY - CONF ID - heimdahl1997usingpvs L3 - citeulike-article-id:5784951 N2 - Previously, we have defined procedures for analyzing hierarchical state based requirements specifications for two properties: (1) completeness with respect to a set of criteria related to robustness (a response is specified for every possible input and input sequence) and (2) consistency (the specification is free from conflicting requirements and undesired nondeterminism) (M.P.E. Heimdahl and N.G. Leveson, 1995; 1996). We implemented the analysis procedures in a prototype tool and evaluated their effectiveness and efficiency on a large real world requirements specification expressed in an hierarchical state based language called RSML (Requirements State Machine Language). Although our approach has been largely successful, there are some drawbacks with the current implementation that must be addressed. Our prototype implementation uses Binary Decision Diagrams (BDDs) to perform the analysis. Unfortunately, since BDDs treat predicates and functions as uninterpreted and thus fail to capture their semantics, the use of BDDs can lead to large numbers of spurious (false) error reports. We are currently investigating how the Prototype Verification System (PVS) and its theorem proving component can help us increase the accuracy of our analysis. PVS is a verification system that provides an interactive environment for writing formal specifications and checking formal proofs. The paper discusses the problems with spurious error reports and describes our experiences using the Prototype Verification System to increase the accuracy of our analysis results JF - High-Assurance Systems Engineering Workshop, 1996. Proceedings., IEEE EP - 262 TI - Using PVS to analyze hierarchical state-based requirements for completeness and consistency SP - 252 KW - requirements AU - Heimdahl, MPE AU - Czerny, BJ PY - 2002/08/06/ UR - http://dx.doi.org/10.1109/HASE.1996.618606 ER -