Applying Infinite State Model Checking and Other Analysis Techniques to Tabular Requirements Specifications of Safety-Critical Systems

2006 ◽  
Author(s):  
Tevfik Bultan ◽  
Constance Heitmeyer
Keyword(s):  
Model Checking ◽  
State Model ◽  
Critical Systems ◽  
Safety Critical ◽  
Analysis Techniques ◽  
Requirements Specifications ◽  
Safety Critical Systems ◽  
Infinite State

scholarly journals Model Checking Safety-Critical Systems Using Safecharts

2007 ◽  
Vol 56 (5) ◽  
pp. 692-705 ◽  
Author(s):  
Pao-Ann Hsiung ◽  
Yean-Ru Chen ◽  
Yen-Hung Lin
Keyword(s):  
Model Checking ◽  
Critical Systems ◽  
Safety Critical ◽  
Safety Critical Systems

DEBUGGING LOGIC-BASED REQUIREMENTS SPECIFICATIONS FOR SAFETY-CRITICAL SYSTEMS — A FRORL APPROACH

1994 ◽  
Vol 04 (02) ◽  
pp. 205-228 ◽  
Author(s):  
JEFFREY J.P. TSAI ◽  
ALAN LIU ◽  
KRISHNAKUMAR NAIR
Keyword(s):  
Timing Constraints ◽  
Critical Systems ◽  
Testing And Debugging ◽  
Safety Critical ◽  
Requirements Specifications ◽  
Safety Critical Systems ◽  
Deterministic Behavior

Safety-critical systems are not only difficult to build, but also difficult to debug because they often have strict timing constraints and non-deterministic behavior. A correct and precise specification reduces the effort spent in testing and debugging the implemented system. This paper presents techniques of specification debugging and issues related to it. We introduce an approach to the debugging of a specification in FRORL (Frame and Rule Oriented Requirements Language), which supports non-determinism and non-monotonicity in a system. The approach aids the user in detecting and correcting the possible faults which can arise not only when writing the specification, but also after the verification of the specification.

Sign in / Sign up

Export Citation Format

Share Document