Paper Authors

Abstract

NOTE: The first page of text has been automatically extracted and included below in lieu of an abstract

Experiment to Evaluate Teaching Formal Specifications Using Model Checking

Salamah Salamah Computer and Software Engineering Dept., Embry-Riddle Aeronautical University. Steve Roach, Veronica Medina, Omar Ochoa, and Ann Gates Computer Science Dept., University of Texas at El Paso.

Abstract

The difficulty of writing, reading, and understanding formal specifications remains one of the main obstacles in adopting formal verification techniques such as model checking, theorem and runtime verification. In order to train a future workforce that can develop and test high-assurance systems, it is essential to introduce undergraduate students in computer science and software en- gineering to the concepts in formal methods. This paper presents an experiment that we used to validate the effectiveness of a new approach that can be used in an undergraduate course to teach formal approaches and languages. The paper presents study that was conducted at two institutions to compare the new approach with the traditional one in teaching formal specifications. The new approach 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.

1 Introduction

In software engineering, formal techniques such as software runtime monitoring [5], and model checking [3, 8] require formal specifications that are based on mathematics. Formally specifying the behavior of a software system, however, is a difficult task because it requires mathematical sophis- tication to accurately specify, read, and understand properties written in a formal language. Natural language descriptions of software requirements are inherently ambiguous and often incomplete. Deriving a formal specification from a requirement written in natural-language of concurrent or sequential behavior is made more difficult because of the variety of aspects that must be considered when specifying software behavior. As such, a major impediment to the use of formal approaches in software development remains the difficulty associated with the development of correct formal specifications (i.e, ones that match the specifier’s original intent) [6, 7]. Currently, there exists multiple formal specification languages that can be used in a variety of verification techniques and tools. Linear Temporal Logic (LTL) [11], Computational Tree Logic (CTL) [10], and Meta Event Definition Language (MEDL) [9] are some of these languages. The aforementioned languages can be used in a variety of verification techniques and tools. For exam- ple, the model checkers SPIN [8] and NuSMV [2] use LTL to specify properties of software and hardware systems. On the other hand, the SMV [3] model checker verifies system behaviors against formal properties in in CTL. MEDL is used by JavaMac in runtime monitoring of java programs [9]. Many undergraduate curricula do not include the topic of formal methods. Certainly, a high level of mathematical sophistication is required for writing, reading, and understanding formal specifi-

1

• Citation

• Format
  • APA
  • APA - LaTeX bibitem
  • MLA
  • MLA - LaTeX bibitem
  • Bibtex
  • EndNote - RIS

Salamah, S., & Roach, S., & Ochoa, O., & Medina, V., & Gates, A. (2009, June), An Experiment To Evaluate An Approach To Teaching Formal Specifications Using Model Checking Paper presented at 2009 Annual Conference & Exposition, Austin, Texas. 10.18260/1-2--5809