FORMAL MODELING OF COMPLEX COMMANDS IN INDUSTRIAL SOFTWARE SPECIFICATIONS

We present a formal approach for modeling complex commands characteriz ed by heavy overloading of function, large numbers of parameters, depe ndencies among parameters, subtle side effects, and lack of abstractio n. Complex commands arise in a variety of business settings such as re questing a brokerage order, enrolling in a course, and specifying a pr oduct order. In addition, complex commands are also prevalent where sp ecification of commands is strictly separated from multiple, independe nt implementations as in open software standards. Our approach is base d on an inheritance structure known as a command lattice. Like other f orms of inheritance, command lattices support incremental definition a nd abbreviation of specifications. Because a complete command lattice can have a large number of specifications, we develop another structur e known as a minimal command tree in which a command lattice is derive d from a much smaller number of independent specifications. To map fro m a minimal command tree to a command lattice, we present algorithms t hat materialize an arbitrary node of a command lattice and compactly g enerate the behavior of a command lattice. To demonstrate the potentia l of command lattices, we have implemented a set of tools that provide convenient specification and powerful reasoning capabilities. Our too l collection includes the Command Specification Language that supports a precise and rich specification of the structural and behavioral pro perties of commands, the incremental definition tool that ensures cons istency of command lattices, the browsing tool that displays a command 's inheritance structure, the type checker that ensures structural con sistency of commands in expressions, and the target system tracer that simulates a sequence of command executions. We discuss our experience s applying the tools to IBM's Distributed Data Management, a large sca le specification of data access on remote and heterogeneous IBM system s.