Asee peer logo

An Experiment To Evaluate An Approach To Teaching Formal Specifications Using Model Checking

Download Paper |


2009 Annual Conference & Exposition


Austin, Texas

Publication Date

June 14, 2009

Start Date

June 14, 2009

End Date

June 17, 2009



Conference Session

Software Engineering Teaching Techniques

Tagged Division

Software Engineering Constituent Committee

Page Count


Page Numbers

14.192.1 - 14.192.13

Permanent URL

Download Count


Request a correction

Paper Authors

author page

Salamah Salamah Embry-Riddle Aeronautical University, Daytona Beach

author page

Steve Roach University of Texas, El Paso

author page

Omar Ochoa University of Texas, El Paso

author page

Veronica Medina University of Texas, El Paso

author page

Ann Gates University of Texas, El Paso

Download Paper |

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.


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-


ASEE holds the copyright on this document. It may be read by the public free of charge. Authors may archive their work on personal websites or in institutional repositories with the following citation: © 2009 American Society for Engineering Education. Other scholars may excerpt or quote from these materials with the same citation. When excerpting or quoting from Conference Proceedings, authors should, in addition to noting the ASEE copyright, list all the original authors and their institutions and name the host city of the conference. - Last updated April 1, 2015