Computer Science Seminar Series
A Formal Language and Analysis Tool for Black Box Specifications
Februray 13, 3:00pm
Weir Hall, Room 235
Gabriel J. Ferrer, PhD
Assistant Professor of Computer Science
Hendrix College
Abstract:
Many errors in software can be attributed to the failure to properly specify a response for an input scenario. In order to address this problem, I am developing a formal specification language and analysis tool for modeling the boundary between a software artifact and its environment. The prototype analysis tool that I have developed has been employed in software engineering courses at two different institutions. The experiences from the classroom have demonstrated that the specification language is easy to learn in a short period of time, and that the language is sufficiently expressive to represent several interesting GUI-based desktop application programs. Some preliminary applications of this specification language to problems in robotics will also be presented.
The language is inspired by the black box specification method developed by Harlan Mills and his colleagues as part of the Cleanroom Software Engineering process. In this language, each black box specification is represented by a table that indicates how the artifact responds to a particular input from the environment. This response depends not only on the current input, but also on the entire history of interactions it has had with the environment.
The analysis tool verifies whether a black box is a well-formed specification. To this end, it ensures that a response is specified for every possible combination of inputs from the environment, that every condition is logically disjoint with every other condition in the specification, and that every condition in the specification matches at least one potential input scenario.