June 14, 2009
June 14, 2009
June 17, 2009
Software Engineering Constituent Committee
14.192.1 - 14.192.13
Experiment to Evaluate Teaching Formal Speciﬁcations 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 difﬁculty of writing, reading, and understanding formal speciﬁcations remains one of the main obstacles in adopting formal veriﬁcation techniques such as model checking, theorem and runtime veriﬁcation. 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 speciﬁcations. The new approach uses a model checker and a speciﬁcation tool to teach Linear Temporal Logic (LTL), a speciﬁcation language that is widely used in a variety of veriﬁcation tools.
In software engineering, formal techniques such as software runtime monitoring , and model checking [3, 8] require formal speciﬁcations that are based on mathematics. Formally specifying the behavior of a software system, however, is a difﬁcult 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 speciﬁcation from a requirement written in natural-language of concurrent or sequential behavior is made more difﬁcult 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 difﬁculty associated with the development of correct formal speciﬁcations (i.e, ones that match the speciﬁer’s original intent) [6, 7]. Currently, there exists multiple formal speciﬁcation languages that can be used in a variety of veriﬁcation techniques and tools. Linear Temporal Logic (LTL) , Computational Tree Logic (CTL) , and Meta Event Deﬁnition Language (MEDL)  are some of these languages. The aforementioned languages can be used in a variety of veriﬁcation techniques and tools. For exam- ple, the model checkers SPIN  and NuSMV  use LTL to specify properties of software and hardware systems. On the other hand, the SMV  model checker veriﬁes system behaviors against formal properties in in CTL. MEDL is used by JavaMac in runtime monitoring of java programs . 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 speciﬁ-
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