Data Refinement for Synchronous System Specification and Construction

  • Alex Tsow
  • Steven D. Johnson
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3725)


Design derivation, a correct-by-construction system design method, specifies behavior with abstract datatypes. Refining these abstract datatypes is necessary for architectural decomposition. A new transformation primitive enables data refinement by generalizing term level injective homomorphisms to system equivalence.


  1. 1.
    Johnson, S.D.: Manipulating logical organization with system factorizations. In: Leeser, M., Brown, G. (eds.) Hardware Specification, Verification and Synthesis: Mathematical Aspects. LNCS, vol. 408. Springer, Heidelberg (1990)Google Scholar
  2. 2.
    Johnson, S.D., Tsow, A.: Algebra of behavior tables. In: Lfm2000: Fifth NASA Langley Formal Methods Workshop, Proceedings (2000)Google Scholar
  3. 3.
    Miner, P.S.: Hardware Verification using Coinductive Assertions. PhD thesis, Computer Science Department, Indiana University, USA (June 1998), T.R. No. 510Google Scholar
  4. 4.
    Tsow, A., Johnson, S.D.: Visualizing system factorizations with behavior tables. In: Johnson, S.D., Hunt Jr., W.A. (eds.) FMCAD 2000. LNCS, vol. 1954, pp. 520–537. Springer, Heidelberg (2000)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Alex Tsow
    • 1
  • Steven D. Johnson
    • 1
  1. 1.System Design Methods Laboratory, Computer Science DepartmentIndiana University 

Personalised recommendations