This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Using a Protean Language to Enhance Expressiveness in Specification
April 1997 (vol. 23 no. 4)
pp. 224-234

Abstract—A Protean specification language [6] based on Structured Operational Semantics (SOS) allows the user to invent appropriate operations to improve abstraction and readability. This is in contrast to traditional specification languages, where the set of operations is fixed. An efficient algorithm, described in [10], uses binary decision diagrams (BDDs) to verify properties of finite specifications written in a Protean language and provides the basis for a model checker we have developed. This paper provides a synthesis of our work on Protean languages and relates the work to other specification techniques. We show how abstraction and refinement in the Protean framework can improve the effectiveness of model checking. We rewrite and verify properties of an existing Z specification by defining suitable operations. We also show how a Protean language can be used to model restricted I/O automata, action refinement, and 1-safe and k-bounded Petri nets.

[1] L. Aceto, "GSOS and Finite Labelled Transition Systems," Technical Report 6/93, Univ. of Sussex at Brighton, Mar. 1993.
[2] L. Aceto and M. Henessy, "Towards Action-Refinement in Process Algebras," LICS '89, 1989.
[3] E. Brinksma and T. Bolognesi, "Introduction to the ISO Specification Language LOTOS," Computer Networks and ISDN Systems, vol. 14, pp. 25-59, 1987.
[4] J. Burch, E. Clarke, and D. Long, "Symbolic Model Checking with Partitioned Transition Relations," VLSI '91,Edinburgh, Scotland, 1991.
[5] B. Bloom, "Ready Simulation, Bisimulation, and the Semantics of CCS-Like Languages," PhD thesis, Mass. Inst. of Tech., Sept. 1989.
[6] B. Bloom, "Structural Operational Semantics Considered as a Specification Language," Proc. POPL '95, pp. 107-117. IEEE Press, 1995.
[7] J.C.M. Baeten and W.P. Weijland, Process Algebra, Cambridge Tracts in Theoretical Computer Science 18. Cambridge Univ. Press, 1990.
[8] R. Cleaveland, "The NCSU Concurrency Workbench," Computer Aided Verification, 1996.
[9] K.M. Chandy and J. Misra, Parallel Program Design—A Foundation. Addison-Wesley, 1988.
[10] A. Dsouza and B. Bloom, "Generating BDD Models for Process Algebra Terms," P. Wolper, ed., Computer Aided Verification: Seventh Int'l Conf.,Liege, Belgium, pp. 16-30. Springer-Verlag, July 1995.
[11] A. Dsouza and B. Bloom, "On the Expressive Power of CCS," P.S. Thiagarajan, ed., Foundations of Software Technology and Theoretical Computer Science,Bangalore, India, Lecture Notes in Computer Science, 1026, Springer-Verlag, Dec. 1995.
[12] E.W. Dijkstra, "Guarded Commands, Nondeterminacy, and Formal Derivation of Programs," Comm. ACM, vol. 18, no. 8, pp. 453-457, Aug 1975.
[13] A. Dsouza, "Model Checking and Expressiveness for First Order Process Algebras," PhD thesis, Cornell Univ., Ithaca, New York, Aug. 1996.
[14] R. Enders, T. Filkhorn, and D. Taubner, "Generating BDDs for Symbolic Model Checking in CCS," Distributed Computing, vol. 6, pp. 155-164, 1993.
[15] A. Evans, "Specifying and Verifying Concurrent Systems Using Z," Formal Methods Europe '94, Lecture Notes in Computer Science, pp. 366-380, Springer-Verlag, 1994.
[16] C.A.R. Hoare, Communicating Sequential Processes, Prentice Hall, Englewood Cliffs, N.J., 1985.
[17] N. Lynch and R. Segala, "A Comparison of Simulation Techniques and Algebraic Techniques for Verifying Concurrent Systems," B. Bloom, ed., Proc. North American Process Algebra Workshop '93. Cornell Technical Report, 1993.
[18] N.A. Lynch and M.R. Tuttle, "Hierarchical Correctness Proofs for Distributed Algorithms," Proc. Sixth Symp. Principles of Distributed Computing, pp. 137-151, ACM, New York, 1987.
[19] R. Milner, "Calculi for Synchrony and Asynchrony," Theoretical Computer Science, vol. 25, pp. 267-310, 1983.
[20] R. Milner, Communication and Concurrency. Prentice Hall, 1989.
[21] G. Plotkin, "A Structural Approach to Operational Semantics," Technical Report DAIMI FN-19, Aarhus Univ., Computer Science Dept., Denmark, 1981.
[22] W. Reisig, Petri Nets. Springer-Verlag, 1985.

Index Terms:
Formal methods, specification, verification, structured operational semantics, process algebra, model checking.
Citation:
Bard Bloom, Allan Cheng, Ashvin Dsouza, "Using a Protean Language to Enhance Expressiveness in Specification," IEEE Transactions on Software Engineering, vol. 23, no. 4, pp. 224-234, April 1997, doi:10.1109/32.588539
Usage of this product signifies your acceptance of the Terms of Use.