Controllable Delay-Insensitive Processes

• Autorzy: Josephs M.B. , Kapoor H.K.
• Języki publikacji: EN

Abstrakty

EN

Josephs and Udding's DI-Algebra offers a convenient way of specifying and verifying designs that must rely upon delay-insensitive signalling between modules (asynchronous logic blocks). It is based on Hoare's theory of CSP, including the notion of refinement between processes, and is similarly underpinned by a denotational semantics. Verhoeff developed an alternative theory of delay-insensitive design based on a testing paradigm and the concept of reflection. The first contribution of this paper is to define a relation between processes in DI-Algebra that captures Verhoeff's notion of a closed system passing a test (by being free of interference and deadlock). The second contribution is to introduce a new notion of controllability, that is, to define what it means for a process to be controllable in DI-Algebra. The third contribution is to extend DI-Algebra with a reflection operator and to show how testing relates to controllability, reflection and refinement. It is also shown that double reflection yields fully-abstract processes in the sense that it removes irrelevant distinctions between controllable processes. The final contribution is a modified version of Verhoeff's factorisation theorem that could potentially be of major importance for constructive design and the development of design tools. Several elementary examples are worked out in detail to illustrate the concepts. The claims made in this paper are accompanied by formal proofs, mostly in an annotated calculational style.

Słowa kluczowe

EN

process algebras; refinement; testing; controllability; reflection; factorisation

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2007
• Tom: Vol. 78, nr 1
• Strony: 101--130
• Opis fizyczny: bibliogr. 30 poz., tab., wykr.

Twórcy

autor

Josephs M.B.

autor

Kapoor H.K.

• Faculty of BCIM, London South Bank University, 103 Borough Road, London SEI 0AA, UK,

Bibliografia

• [1] Benko, I., Ebergen, J.: Composing Snippets, in: Concurrency and Hardware Design: Advances in Petri Nets, Lecture Notes in Computer Science (J. Cortadella, A. Yakovlev, G. Rozenberg, Eds.), 2549, 2002, 1-33.
• [2] v. Bochmann, G.: Submodule Construction and Supervisory Control: A Generalization, Proc. Sixth International Conference on Implementation and Application of Automata, Lecture Notes in Computer Science, 2494, 2001, 27-39.
• [3] Clavel, M., Eker, S., Lincoln, P., Meseguer, J.: Principles of Maude, Electronic Notes in Theoretical Computer Science, 4, 1996, 65-89.
• [4] Cortadella, J., Kishinevsky,M., Kondratyev, A., Lavagno, L., Yakovlev, A.: Petrify: A Tool forManipulating Concurrent Specifications and Synthesis of Asynchronous Controllers, IEICE Transactions on Information and Systems, 3(E80-D), 1997, 315-325.
• [5] Dill, D. L.: Trace Theory for Automatic Hierarchical Verification of Speed-Independent Circuits, ACM Distinguished Dissertations. MIT Press, 1989.
• [6] Drissi, J., v. Bochmann, G.: Submodule Construction for Systems of I/O Automata, http://citeseer.ist.psu.edu/229830.html, 1999.
• [7] Groenboom, R., Josephs,M. B., Lucassen, P. G., Udding, J. T.: Normal Form in a Delay-Insensitive Algebra, in: Asynchronous Design Methodologies, IFIP Transactions (S. Furber, M. Edwards, Eds.), A-28, 1993, 57-70.
• [8] Hennessy, M.: Algebraic Theory of Processes, MIT Press, 1988.
• [9] Hoare, C. A. R.: Communicating Sequential Processes, Prentice-Hall International Series in Computer Science, 1985.
• [10] Josephs, M. B.: Receptive Process Theory, Acta Informatica, 29(1), 1992, 17-31.
• [11] Josephs, M. B., Furey, D. P.: Delay-Insensitive Interface Specification and Synthesis, Proc. Design, Automation and Test in Europe (DATE), IEEE Computer Society, 2000, 169-173.
• [12] Josephs, M. B., Furey, D. P.: A Programming Approach to the Design of Asynchronous Logic Blocks, in: Concurrency and Hardware Design: Advances in Petri Nets, Lecture Notes in Computer Science (J. Cortadella, A. Yakovlev, G. Rozenberg, Eds.), 2549, 2002, 34-60.
• [13] Josephs, M. B., Hoare, C. A. R., He, J.: A Theory of Asynchronous Processes, Technical Report PRG-TR-6-89, Oxford University Computing Laboratory, Oxford, England, 1989.
• [14] Josephs, M. B., Udding, J. T.: An Overview of D-I Algebra, Proc. Twenty-Sixth Hawaii International Conference on System Sciences, IEEE Computer Society, 1993, 329-338.
• [15] Kapoor, H. K.: Delay Insensitive Processes: A Formal Approach to the Design of Asynchronous Circuits, Ph.D. Thesis, London South Bank University, UK, July 2004.
• [16] Kapoor, H. K., Josephs, M. B., Furey, D. P.: Verification and Implementation of Delay-Insensitive Processes in Restrictive Environments, Fundamenta Informaticae, 70(1-2), January 2006, 21-48.
• [17] Lucassen, P. G.: A Denotational Model and Composition Theorems for a Calculus of Delay-Insensitive Specifications, Ph.D. Thesis, Dept. of C.S., Univ. of Groningen, The Netherlands,May 1994.
• [18] Lucassen, P. G., Polak, I., Udding, J. T.: Normal Form in DI-Algebra with Recursion, Proc. Third International Symposium on Advanced Research in Asynchronous Circuits and Systems, IEEE Computer Society, 1997, 167-174.
• [19] Mallon, W. C.: Theories and Tools for the Design of Delay-Insensitive Communicating Processes, Ph.D. Thesis, Dept. of C.S., Univ. of Groningen, The Netherlands, January 2000.
• [20] Mallon, W. C., Udding, J. T., Verhoeff, T.: Analysis and Applications of the XDI model, Proc. Fifth International Symposium on Advanced Research in Asynchronous Circuits and Systems, IEEE Computer Society, 1999, 231-242.
• [21] Merlin, P., v. Bochmann, G.: On the Construction of Submodule Specifications and Communication Protocols, ACM Transactions on Programming Languages and Systems, 5(1), January 1983, 1-25.
• [22] Milner, R.: A Calculus of Communicating Systems, Lecture Notes in Computer Science, 92, 1980.
• [23] Molnar, C. E., Fang, T. P., Rosenberger, F. U.: Synthesis of Delay-Insensitive Modules, in: Chapel Hill Conference on Very Large Scale Integration (H. Fuchs, Ed.), Computer Science Press, 1985, 67-86.
• [24] Negulescu, R.: General Testers for Asynchronous Circuits, Proc. 10th IEEE International Symposium on Asynchronous Circuits and Systems, IEEE Computer Society, 2004, 28-38.
• [25] Nicola, R. D., Hennessy, M.: Testing equivalence for processes, Theoretical Computer Science, 34, 1984, 83-133.
• [26] Parrow, J.: Submodule Construction as Equation Solving in CCS, Theoretical Computer Science, 68(2), October 1989, 175-202.
• [27] Udding, J. T.: A Formal Model for Defining and Classifying Delay-Insensitive Circuits, Distributed Computing, 1(4), 1986, 197-204.
• [28] Verhoeff, T.: A Theory of Delay-Insensitive Systems, Ph.D. Thesis, Dept. ofMath. and C.S., EindhovenUniv. of Technology,May 1994.
• [29] Verhoeff, T.: Analyzing Specifications for Delay-Insensitive Circuits, Proc. Fourth International Symposium on Advanced Research in Asynchronous Circuits and Systems, IEEE Computer Society, 1998, 172-183.
• [30] Yakovlev, A. V., Koelmans, A. M., Semenov, A., Kinniment, D. J.: Modelling, Analysis and Synthesis of Asynchronous Control Circuits using Petri Nets, Integration, the VLSI Journal, 21(3), December 1996, 143-170.