Search

The Property Specification (Prospec) tool uses patterns and scopes defined by Dwyer et al., to generate formal specifications in Linear Temporal Logic (LTL) and other languages. The work presented in this paper provides improved LTL specifications for patterns and scopes over those originally provided by Prospec. This improvement comes in the efficiency of the LTL formulas as measured in terms of the number of states in the Büchi automaton generated for the formula. Minimizing the size of the Büchi automata for an LTL specification provides a significant improvement for model checking software systems using such tools as the highly acclaimed Spin model checker.

In this paper we present an approach used to enhance students' competency in software verification. Students were asked to apply software verification techniques to a complex formal specification system. The complexity of the system stems from its sophisticated requirements. Selecting such system for this study was intentional for the following two reasons 1) the system is difficult to understand and analyze because of the domain knowledge required to generate formal specifications in temporal logic and 2) the system is large and complex which lends itself to a wide range of applicable verification techniques, and thus highlights the differences in the capabilities of each of the software verification approaches. Students were assessed using multiple criteria including; examination in applying learned techniques, students' attitude toward the technique, perceived efficiency of the techniques in discovering software defects, and the ability of the technique to locate errors in the code beyond simply indicating their presence. The results of this work show that the students applied the learned techniques successfully and their attitudes towards software verification improved.

In this paper, we report on the effectiveness of the testing approach known as pairwise or orthogonal testing in verifying the correctness of the LTL specifications generated by the PROperty SPECification (Prospec) tool. This tool assists the user in generating a large number (over 34,000) of formal specifications in formal languages, including Linear Temporal Logic (LTL). Pairwise testing is a technique that aims at, significantly, reducing the amount of test cases required for testing a particular software system while providing assurance of adequate coverage of the problem space.

Although many software engineering (SE) and computer science (CS) texts use case studies to explain the different concepts, these case studies tend to focus on a specific subject such as object oriented design and implementation or requirements analysis and specification. In addition, these case studies usually lack instructor guidelines on how to use the material in teaching these concepts. The Digital Home Case Study addresses these issues by providing a complete set of artifacts associated with software development, and an extensive set of case study exercises for teaching different topics in software engineering and computer science, as well as guidance for instructors on how to use these case modules. In this paper, we motivate the use of the case study approach in teaching SE and CS concepts. We provide a description of the Digital Home case study and the associated artifacts and case modules. We also report on our use of the developed material.

The use of formal methods in software engineering has been shown to be an effective way to improving the dependability of developed systems. The difficulty of writing, reading, and understanding formal specifications, which is an essential component of formal verification, remains one of the main obstacles in the adoption of formal methods in industry. It is, thus, essential that undergraduate students in computing programs learn how to specify formal system properties. This paper outlines an instructive component that uses a tool to support the teaching of formal approaches and languages, and it presents educational outcomes from using such a component in undergraduate courses. The component uses a model checking-based tool LTLV to teach Linear Temporal Logic (LTL), a well-known specification language. In addition, this paper describes two experiments that compare the effectiveness of the new approach to that of the traditional lecture-based approach. The results of the experiments show promise that the tool-based approach can be effective in teaching formal specifications. The paper provides analysis of the results of the studies, as well as lessons learned from the experiments.

The Property Specification (Prospec) tool uses patterns and scopes defined by Dwyer et. al., to generate formal specifications in linear temporal logic (LTL) and other languages. The work presented in this paper provides improved LTL specifications for patterns and scopes over those originally provided by Prospec. This improvement comes in the efficiency of the LTL formulas as measured in terms of the number of states in the Buchi automaton generated for the formula. Minimizing the size of the Buchi automata for an LTL specification provides a significant support to the area of model checking.

The difficulty of writing, reading, and understanding formal specifications is one of the main obstacles in adopting formal verification techniques such as model checking and runtime verification. Introducing concepts in formal methods in an undergraduate program is essential for training a workforce that can develop and test high-assurance systems. This paper presents educational outcomes and outlines an instructive component that can be used in an undergraduate course to teach formal approaches and languages. The component uses a model checker and a specification tool to teach Linear Temporal Logic (LTL), a specification language that is widely used in a variety of verification tools. The paper also introduces a novel technique that analyzes LTL specifications by using the SPIN model checker to elucidate the behaviors accepted by the specifications.

Property classifications and patterns, i.e., high-level abstractions that describe common behavior, have been used to assist practitioners in generating formal specifications that can be used in formal verification techniques. The Specification Pattern System (SPS) provides descriptions of a collection of patterns. Each pattern is associated with a scope that defines the extent of program execution over which a property pattern is considered. Based on a selected pattern, SPS provides a specification for each type of scope in multiple formal languages including Linear Temporal Logic (LTL). The (Prospec) tool extends SPS by introducing the notion of Composite Propositions (CP), which are classifications for defining sequential and concurrent behavior to represent pattern and scope parameters. In this work, we provide definitions of patterns and scopes when defined using CP classes. In addition, we provide general (template) LTL formulas that can be used to generate LTL specifications for all combinations of pattern, scope, and CP classes.

The use of property classifications and patterns, i.e., high-level abstractions that describe common behavior, have been shown to assist practitioners in generating formal specifications that can be used in formal verification techniques. The specification pattern system (SPS) provides descriptions of a collection of patterns. The extent of program execution over which a pattern must hold is described by the notion of scope. SPS provides a manual technique for obtaining formal specifications from a pattern and a scope. The property specification tool (Prospec) extends SPS by introducing composite propositions (CPs), a classification for defining sequential and concurrent behavior to represent pattern and scope parameters, and provides a tool to support users. This work provides general templates for generating formal specifications in linear temporal logic (LTL) for all pattern, scope, and CP combinations. In addition, the work explains the methodology for the verification of the correctness of these templates.

The Specification Pattern System (SPS) and the Property Specification (Prospec) tool assist a user in generating formal specifications in Linear Temporal Logic (LTL), as well as other languages, from property patterns and scopes. Patterns are high-level abstractions that provide descriptions of common properties, and scopes describe the extent of program execution over which the property holds. The purpose of the work presented in this paper is to verify that the generated LTL formulas match the natural language descriptions, timelines, and traces of computation that describe the pattern and scope. The LTL formulas were verified using the Spin model checker on test cases developed using boundary value analysis and equivalence class testing strategies. A test case is an LTL formula and a sequence of Boolean valuations. The LTL formulas were those generated from SPS and Prospec. The Boolean valuations of propositions in the LTL formula are generated by a deterministic, single-threaded Promela program that was run using the software model-checker Spin. For each pattern, a suite of test cases was. The experiments uncovered several errors in both the SPS-generated and the Prospec-generated formulas.