The Mathematical Laws of S*M: An Axiomatic Specification Language for Firmware and Architecture Design.

点击翻译按钮获取中文摘要

The main results of the PI's work to date are the design and implementation of a novel axiomatic, non-procedural language called S*M for the functional specification of firmware and computer architectures. The implementation of S*M consists of a compiler, a simulator, and a user interface running on VAX 11/780 UNIXTM environment. S*M has been used extensively to specify the behavior of, and reason about, firmware and architectures and, consequently, considerable understanding of its strengths and limitations has been gained. The features of the language have also made it sufficiently attractive for S*M to have influenced research projects in Colorado State University (firmware engineering), University of Guelph, Ontario, Canada (design automation), and the Technical University of Aachen, West Germany (formal development of multiprocessor designs). The project continues this work by identifying the basic mathematical laws of S*M. These laws will take the form "P = Q" where, P, Q, are S*M constructs and will mean that, functionally and behaviorally, "P is the same as Q". Thus, given an occurrence of P in an S*M description, one can transform or replace P by the equivalent Q. These mathematical laws will be such that: (i) All correct specifications in S*M must obey these laws. (ii) A correct S*M specification may be transformed into a equivalent (possibly more concise or more efficient) specification by applying these laws.