Formal Modeling of Complex Commands in Industrial Software Specifications

Michael V. Mannino, Sukumar Rathnam, In Jun Choi and Veronica Tseng
Additional contact information
Michael V. Mannino: Department of Management Science, DJ-10, University of Washington, Seattle, Washington 98195
Sukumar Rathnam: Scopus Technology, 1900 Powell Drive, Suite 900, Emeryville, California 95608
In Jun Choi: Department of Industrial Engineering, Pohang Institute of Science and Technology, P.O. Box 125, Pohang 790-600, Korea
Veronica Tseng: IBM Corporation, 472 Wheelers Farms Road, Mail Drop 61, Milford, Connecticut 06460

Information Systems Research, 1994, vol. 5, issue 3, 249-274

Abstract: We present a formal approach for modeling complex commands characterized by heavy overloading of function, large numbers of parameters, dependencies among parameters, subtle side effects, and lack of abstraction. Complex commands arise in a variety of business settings such as requesting a brokerage order, enrolling in a course, and specifying a product order. In addition, complex commands are also prevalent where specification of commands is strictly separated from multiple, independent implementations as in open software standards.Our approach is based on an inheritance structure known as a command lattice. Like other forms of inheritance, command lattices support incremental definition and abbreviation of specifications. Because a complete command lattice can have a large number of specifications, we develop another structure known as a minimal command tree in which a command lattice is derived from a much smaller number of independent specifications. To map from a minimal command tree to a command lattice, we present algorithms that materialize an arbitrary node of a command lattice and compactly generate the behavior of a command lattice. To demonstrate the potential of command lattices, we have implemented a set of tools that provide convenient specification and powerful reasoning capabilities. Our tool collection includes the Command Specification Language that supports a precise and rich specification of the structural and behavioral properties of commands, the incremental definition tool that ensures consistency of command lattices, the browsing tool that displays a command's inheritance structure, the type checker that ensures structural consistency of commands in expressions, and the target system tracer that simulates a sequence of command executions. We discuss our experiences applying the tools to IBM's Distributed Data Management, a large scale specification of data access on remote and heterogeneous IBM systems.

Keywords: assertions; inheritance; formal methods; abstraction (search for similar items in EconPapers)
Date: 1994
References: Add references at CitEc
Citations:

Downloads: (external link)
http://dx.doi.org/10.1287/isre.5.3.249 (application/pdf)

Related works:
This item may be available elsewhere in EconPapers: Search for items with the same title.

Export reference: BibTeX RIS (EndNote, ProCite, RefMan) HTML/Text

Persistent link: https://EconPapers.repec.org/RePEc:inm:orisre:v:5:y:1994:i:3:p:249-274

Access Statistics for this article

More articles in Information Systems Research from INFORMS Contact information at EDIRC.
Bibliographic data for series maintained by Chris Asher ().