No Access

REPRESENTATION OF SEMIAUTOMATA BY CANONICAL WORDS AND EQUIVALENCES, PART II: SPECIFICATION OF SOFTWARE MODULES

JANUSZ BRZOZOWSKI

David R. Cheriton School of Computer Science, University of Waterloo, Waterloo, Ontario, Canada N2L 3G1, Canada

Search for more papers by this author

and

HELMUT JÜRGENSEN

Department of Computer Science, The University of Western Ontario, London, Ontario, N6A 5B7, Canada

Institut für Informatik, Universität Potsdam, August-Bebel-Str. 89, 14482 Potsdam, Germany

Search for more papers by this author

https://doi.org/10.1142/S0129054107005133Cited by:6 (Source: Crossref)

Abstract

A theory of representation of semiautomata by canonical words and equivalences was developed in [7]. That work was motivated by trace-assertion specifications of software modules, but its focus was entirely on the underlying mathematical model. In the present paper we extend that theory to automata with Moore and Mealy outputs, and show how to apply the extended theory to the specification of modules. In particular, we present a unified view of the trace-assertion methodology, as guided by our theory. We illustrate this approach, and some specific issues, using several nontrivial examples. We include a discussion of finite versus infinite modules, methods of error handling, some awkward features of the trace-assertion method, and a comparison to specifications by automata. While specifications by trace assertions and automata are equivalent in power, there are cases where one approach appears to be more natural than the other. We conclude that, for certain types of system modules, formal specification by automata, as opposed to informal state machines, is not only possible, but practical.

Keywords:

AMSC: 68N30, 68Q60, 68Q45, 68Q42

References

W. Bartussek and D. L. Parnas, Using Assertions About Traces to Write Abstract Specifications for Software Modules, TR77-012 (Univ. of NC, Chapel Hill, 1977) . Google Scholar
W. Bartussek and D. L. Parnas, Inform. Syst. Methodology, LNCS 65 (Springer, 1978) pp. 211–236. Crossref, Google Scholar
W. Bartussek and D. L. Parnas, Software Fundamentals (Collected Works by D. L. Parnas), eds. D. M. Hoffman and D. M. Weiss (Addison-Wesley, 2001) pp. 9–28. Google Scholar
R. V. Book and F. Otto , String-Rewriting Systems ( Springer , 1993 ) . Crossref, Google Scholar
J. A. Brzozowski, Theoretical Computer Science 356, 46 (2006), DOI: 10.1016/j.tcs.2006.01.040. Crossref, Web of Science, Google Scholar
J. A. Brzozowski and H. Jürgensen, Theory of Deterministic Trace-Assertion Specifications. Tech. Rept. CS-2004-30 (School of Comp. Sci., Univ. of Waterloo, 2004). http://www.cs.uwaterloo.ca/cs-archive/CS-2004/CS-2004.shtml . Google Scholar
J. A. Brzozowski and H. Jürgensen, Int. J. Found. of Computer Science 16(5), 831 (2005), DOI: 10.1142/S0129054105003327. Link, Web of Science, Google Scholar
J. R. Büchi, Archiv für Math. Logik und Grundla-genforschung 6, 91 (1964). Google Scholar
J. R. Büchi , Finite Automata, Their Algebras and Grammars , ed. D. Siefkes ( Springer , 1988 ) . Google Scholar
M. Fowler and K. Scott , UML Distilled – A Brief Guide to the Standard Object Modeling Language , 2nd edn. ( Addison-Wesley , 2000 ) . Google Scholar
J. V. Guttag, E. Horowitz and R. Musser, Current Trends in Programming Methodology IV (Prentice-Hall, 1978) pp. 60–79. Google Scholar
D. Hoffman, IEEE Trans. Computers C34(12), 1102 (1985). Google Scholar
D. Hoffman and R. Snodgrass, IEEE Trans. Software Engineering 14(9), 1243 (1988), DOI: 10.1109/32.6168. Crossref, Web of Science, Google Scholar
M. Iglewski, M. Kubica and J. Madey, Trace Specifications of Nondeterministic Multi-Object Modules, Tech. Rept. TR 95–05 (205) (Institute of Informatics, Warsaw University, Warsaw, Poland, 1995) . Google Scholar
M. Iglewski et al. , TAM'97: The Trace Assertion Method of Module Interface Specification ( 1997 ) , http://w3.uqah.uquebec.ca/iglewski/public_html/TAM/ . Google Scholar
R. Janicki and E. Sekerinski, IEEE Trans. Software Engineering 27(7), 577 (2001), DOI: 10.1109/32.935852. Crossref, Web of Science, Google Scholar
Z. Kohavi , Switching and Finite Automata Theory ( McGraw-Hill , 1978 ) . Google Scholar
N. Kuhn and K. Madlener, A Method for Enumerating Cosets of a Group Presented by a Canonical System, Proc. ACM-SIGSAM Int. Symp. on Symbolic and Algebraic Computation (1989) pp. 338–350. Google Scholar
J. Madey, From Requirement Analysis to Code Verification—a Functional Approach (in Polish), Proc. 8th Conference on Real-Time Systems, eds. T. Szmuc and R. Klimek (Chair of Automatics, AGH University of Science and Technology, Cracow, Poland, 2002) pp. 35–74. Google Scholar
J. McLean, J. ACM 31(3), 600 (1984), DOI: 10.1145/828.829. Crossref, Web of Science, Google Scholar
J. McLean, Journal of Computer Security 1(1), 37 (1992). Crossref, Google Scholar
J. McLean , A General Theory of Composition for Trace Sets closed under Selective Interleaving Functions, Traces , Proc. IEEE Symp. on Research in Security and Privacy ( 1994 ) . Google Scholar
D. L. Parnas and Y. Wang, The Trace Assertion Method of Module Interface Specification, Tech. Rept. 89–261 (Queen's University, C&IS, Telecom. Res. Inst, of Ontario, Kingston, ON, Canada 1989) . Google Scholar
W. Snyder, Efficient Ground Completion: An O(n log n) Algorithm for Generating Reduced Sets of Ground Rewrite Rules Equivalent to a Set of Ground Equations E, Proc. RTA-89, Rewriting Techniques and Applications, LNCS 355, ed. N. Dershowitz (1989) pp. 419–433. Google Scholar
P. H. Starke , Abstract Automata ( North-Holland , Amsterdam , 1972 ) . Google Scholar
Y. Wang, Formal and Abstract Software Module Specifications — A Survey, Tech. Rept. 91–307 (Comp. and Inf. Sci., Queen's University, Kingston, ON, 1991) . Google Scholar
Y. Wang and D. L. Parnas, IEEE Trans. on Software Engineering 20(10), 750 (1994), DOI: 10.1109/32.328996. Crossref, Web of Science, Google Scholar
K. Weidenhauptet al., IEEE Software 15(2), 34 (1998), DOI: 10.1109/52.663783. Crossref, Web of Science, Google Scholar