Impalpable constraints: Framing requirements for formal methods
Travis D. Breaux, Annie I. Antón · NCSU Libraries Repository (North Carolina State University Libraries) · 2007
Regulated software systems require a precise and unambiguous system specification that strictly conforms to the intent of policies and regulations.Formal methods for verification and validation can be used to show that specifications are consistent and complete.However, small and medium sized projects often lack access to the expertise and training required to apply such methods.Towards improving access to formal methods, we introduce a frame-based approach to model requirements that aligns a configurable natural language representation of requirements with a corresponding first-order predicate logic model.The natural language representation supports domain experts and other stakeholders who create, modify or interpret regulatory requirements, whereas the logic model supports machine manipulation of these requirements for automated reasoning.In this paper, we present:1) the frame-based theory; 2) a case study design and associated metrics for evaluating different models in this theory; 3) the results of a case study in the domains of aviation, healthcare and privacy; 4) constraint patterns that were acquired using this approach and that can be re-used to increase consistency in stating requirements; and 5) a prototype that implements the frame-based theory for specification of regulatory requirements.