Enhanced operational semantics

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Enhanced operational semantics: a tool for describing and analyzing concurrent systems

Full text

Pdf (355 KB)

Source

ACM Computing Surveys (CSUR) archive
Volume 33 , Issue 2 (June 2001) table of contents

Pages: 135 - 176

Year of Publication: 2001

ISSN:0360-0300

Authors

Pierpaolo Degano	Univ. di Pisa, Pisa, Italy
Corrado Priami	Univ. di Verona, Verona, Italy

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 9, Downloads (12 Months): 102, Citation Count: 16

Additional Information:

abstract references cited by index terms collaborative colleagues

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/384192.384194 What is a DOI?

ABSTRACT

This article surveys the definition and application of an enhancement of structural operational semantics in the field of concurrent systems, and also addresses issues of distribution and mobility of code. The focus is on how enriching the labels of transitions with encodings of their deduction trees is sufficient to derive qualitative and quantitative information on the systems in hand simply by relabeling the transitions of a unique concrete model.

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	ACETO,L.AND MURPHY, D. 1993. Timing and causality in process algebra. Tech. Rep. 9/93. University of Sussex, Sussex, England.
	2	Roberto M. Amadio , Ilaria Castellani , Davide Sangiorgi, On bisimulations of the asynchronous &pgr;-calculus, Theoretical Computer Science, v.195 n.2, p.291-324, March 30, 1998 [doi>10.1016/S0304-3975(97)00223-5]
	3	Falko Bause , Peter Buchholz , Peter Kemper, QPN-Tool for the Specification ans Analysis of Hierarchically Combined Queueing Petri Nets, Proceedings of the 8th International Conference on Modelling Techniques and Tools for Computer Performance Evaluation: Quantitative Evaluation of Computing and Communication Systems, p.224-238, September 20-22, 1995
	4	Marco Bernardo , Lorenzo Donatiello , Roberto Gorrieri, A formal approach to the integration of performance aspects in the modeling and analysis of concurrent systems, Information and Computation, v.144 n.2, p.83-154, Aug. 1, 1998 [doi>10.1006/inco.1998.2706]
	5	Marco Bernardo , Rance Cleaveland , Steve Sims , W. Stewart, TwoTowers: A Tool Integrating Functional and Performance Analysis of Concurrent Systems, Proceedings of the FIP TC6 WG6.1 Joint International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols (FORTE XI) and Protocol Specification, Testing and Verification (PSTV XVIII), p.457-467, November 03-06, 1998
	6	Bard Bloom, Structured operational semantics as a specification language, Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.107-117, January 23-25, 1995, San Francisco, California, United States [doi>10.1145/199448.199472]
	7	Chiara Bodei , Pierpaolo Degano , Corrado Priami, Names fo the &pgr;-calculus agents handled locally, Theoretical Computer Science, v.253 n.2, p.155-184, Feb. 28, 2001 [doi>10.1016/S0304-3975(00)00093-1]
	8	Chiara Bodei , Pierpaolo Degano , Riccardo Focardi , Corrado Priami, Authentication via Localized Names, Proceedings of the 1999 IEEE Computer Security Foundations Workshop, p.98, June 28-30, 1999
	9	Chiara Bodei , Pierpaolo Degano , Corrado Priami, Constructing Specific SOS Semantics for Concurrency via Abstract Interpretation, Proceedings of the 5th International Symposium on Static Analysis, p.168-183, September 14-16, 1998
	10	BOREALE,M.AND SANGIORGI, D. 1995. A fully abstract semantics of causality in the pi-calculus. In Proceedings of STACS '95. Lecture Notes in Computer Science, Springer-Verlag, New York.
	11	Roberta Borgia , Pierpaolo Degano , Corrado Priami , Lone Leth , Bent Thomsen, Understanding Mobile Agents via a Non-Interleaving Semantics for Facile, Proceedings of the Third International Symposium on Static Analysis, p.98-112, September 24-26, 1996
	12	BOUDOL,G.AND CASTELLANI, I. 1988. A noninterleaving semantics for CCS based on proved transitions. Fund. Inf. XI, 4, 433-452.
	13	G. Boudol , I. Castellani , M. Hennessy , A. Kiehn, Observing localities, Theoretical Computer Science, v.114 n.1, p.31-61, June 14 1993
	14	Jonathan P. Bowen , Michael G. Hinchey, Ten Commandments of Formal Methods, Computer, v.28 n.4, p.56-63, April 1995 [doi>10.1109/2.375178]
	15	BRAVETTI,M.AND GORRIERI, R. 1999. Interactive generalized semi-Markov processes. In Proceedings of PAPM '99. Carleton Scientific.
	16	Mario Bravetti , Marco Bernardo , Roberto Gorrieri, Towards Performance Evaluation with General Distributions in Process Algebras, Proceedings of the 9th International Conference on Concurrency Theory, p.405-422, September 08-11, 1998
	17	BRINKSMA, E., KATOEN, J.-P., LANGERAK, R., AND LATELLA, D. 1995. A stochastic causality based process algebra. Comput. J. 38,6, 552-565.
	18	BRODO, L., DEGANO,P.,AND PRIAMI, C. 2000. A tool for quantitative analysis of pi-calculus processes. In Proceedings of PAPM '00, Carleton Scientific.
	19	BUCHHOLZ, P. 1994. On a Markovian process algebra. Tech. Rep. 500, Informatik IV, University of Dortmund.
	20	Nadia Busi , Roberto Gorrieri, A Petri Net Semantics for pi-Calculus, Proceedings of the 6th International Conference on Concurrency Theory, p.145-159, August 21-24, 1995
	21	Luca Cardelli , Andrew D. Gordon, Mobile Ambients, Proceedings of the First International Conference on Foundations of Software Science and Computation Structure, p.140-155, March 28-April 04, 1998
	22	G. Chiola , G. Franceschinis , R. Gaeta , M. Ribaudo, GreatSPN 1.7: graphical editor and analyzer for timed and stochastic Petri nets, Performance Evaluation, v.24 n.1-2, p.47-68, Nov. 1995 [doi>10.1016/0166-5316(95)00008-L]
	23	D'ARGENIO, P. R. 1999. Algebras and automata for timed and stochastic systems. Ph.D. University of Twente.
	24	Pedro R. D'Argenio , Joost-Pieter Katoen , Ed Brinksma, An algebraic approach to the specification of stochastic systems, Proceedings of the IFIP TC2/WG2.2,2.3 International Conference on Programming Concepts and Methods, p.126-147, June 08-12, 1998
	25	Philippe Darondeau , Pierpaolo Degano, Causal Trees, Proceedings of the 16th International Colloquium on Automata, Languages and Programming, p.234-248, July 11-15, 1989
	26	DE BAKKER,J.W.AND DE ROEVER, W. P. 1972. A calculus for recursive program schemes. In Proceedings of ICALP '72. North-Holland, Amsterdom, The Netherlands, pp. 167-196.
	27	Pierpaolo Degano , Roberto Gorrieri, A causal operational semantics of action refinement, Information and Computation, v.122 n.1, p.97-119, Oct. 1995 [doi>10.1006/inco.1995.1142]
	28	Pierpaolo Degano , Corrado Priami, Proved Trees, Proceedings of the 19th International Colloquium on Automata, Languages and Programming, p.629-640, July 13-17, 1992
	29	Pierpaolo Degano , Corrado Priami, Enhanced operational semantics, ACM Computing Surveys (CSUR), v.28 n.2, p.352-354, June 1996 [doi>10.1145/234528.234748]
	30	Pierpaolo Degano , Corrado Priami, Non-interleaving semantics for mobile processes, Theoretical Computer Science, v.216 n.1-2, p.237-270, March 11, 1999 [doi>10.1016/S0304-3975(99)80003-6]
	31	Pierpaolo Degano , Rocco De Nicola , Ugo Montanari, Partial ordering derivations for CCS, Fundamentals of Computation Theory, p.520-533, September 09-13, 1985
	32	P. Degano , R. De Nicola , U. Montanari, A partial ordering semantics for CCS, Theoretical Computer Science, v.75 n.3, p.223-262, Oct. 1990 [doi>10.1016/0304-3975(90)90095-Y]
	33	Pierpaolo Degano , Corrado Priami , Lone Leth , Bent Thomsen, Analysis of Facile Programs: A Case Study, Selected papers from the 5th LOMAPS Workshop on Analysis and Verification of Multiple-Agent Languages, p.345-369, June 24-26, 1996
	34	DEGANO, P., PRIAMI, C., LETH, L., AND THOMSEN,B. 1999. Causality for debugging mobile agents. Acta Inf. 36, 335-374.
	35	Kate Finney, Mathematical Notation in Formal Specification: Too Difficult for the Masses?, IEEE Transactions on Software Engineering, v.22 n.2, p.158-159, February 1996 [doi>10.1109/32.485225]
	36	Cédric Fournet , Georges Gonthier , Jean-Jacques Lévy , Luc Maranget , Didier Rémy, A Calculus of Mobile Agents, Proceedings of the 7th International Conference on Concurrency Theory, p.406-421, August 26-29, 1996
	37	Sanjiva Prasad , Alessandro Giacalone , Prateek Mishra, Operational and algebraic semantics for Facile: a symmetric integration of concurrent and functional programming, Proceedings of the seventeenth international colloquium on Automata, languages and programming, p.765-780, July 1990, Warwick University, England
	38	Stephen Gilmore , Jane Hillston, The PEPA workbench: a tool to support a process algebra-based approach to performance modelling, Proceedings of the 7th international conference on Computer performance evaluation : modelling techniques and tools: modelling techniques and tools, p.353-368, June 1994, Vienna, Austria
	39	Roberto Gorrieri , Marco Roccetti, Towards Performance Evaluation in Process Algebras, Proceedings of the Third International Conference on Methodology and Software Technology: Algebraic Methodology and Software Technology, p.289-296, June 21-25, 1993
	40	GOTZ, N., HERZOG,U.,AND RETTELBACH, M. 1992. TIPP-A language for timed processes and performance evaluation. Tech. Rep. 4/92. IMMD VII, University of Erlangen-Nurnberg.
	41	HARRISON,P.GAND STRULO, B. 1995. Stochastic process algebra for discrete event simulation. In Quantitative Methods in Parallel Systems, Springer Verlag Esprit Badie Research Series, pp. 18-37.
	42	Matthew Hennessy, Algebraic theory of processes, MIT Press, Cambridge, MA, 1988
	43	Jane Hillston, A compositional approach to performance modelling, Cambridge University Press, New York, NY, 1996
	44	C. A. R. Hoare, Communicating sequential processes, Prentice-Hall, Inc., Upper Saddle River, NJ, 1985
	45	INVERARDI,P.AND PRIAMI, C. 1996. Automatic verification of distributed systems: The process algebras approach. Form. Meth. Syst. Des. 8,1, 1-37.
	46	Lalita Jategaonkar, Observing “true” concurrency, Massachusetts Institute of Technology, Cambridge, MA, 1993
	47	Lalita Jategaonkar Jagadeesan , Radha Jagadeesan, Causality and True Concurrency: A Data-flow Analysis of the Pi-Calculus (Extended Abstract), Proceedings of the 4th International Conference on Algebraic Methodology and Software Technology, p.277-291, July 03-07, 1995
	48	Cliff B. Jones, Systematic software development using VDM (2nd ed.), Prentice-Hall, Inc., Upper Saddle River, NJ, 1990
	49	KATOEN, J.-P. 1996. Quantitative and qualitative extensions of event structures. Ph.D. dissertation. Center for Telematics and Information Technology, University of Twente. Available as CTIT No. 96-09.
	50	A. Kiehn, Comparing locality and causality based equivalences, Acta Informatica, v.31 n.9, p.697-718, Nov. 1994
	51	LANDIN, P. 1964. The mechanical evaluation of expressions. Comput. J. 6,4.
	52	Kim Guldstrand Larsen , Arne Skou, Compositional Verification of Probabilistic Processes, Proceedings of the Third International Conference on Concurrency Theory, p.456-471, August 24-27, 1992
	53	LUCAS, P. 1971. Formal definition of programming languages and systems. In Proceedings of IFIP '71.
	54	Andrea Maggiolo-Schettini , Simone Tini, Applying techniques of asynchronous concurrency to synchronous languages, Fundamenta Informaticae, v.40 n.2-3, p.221-250, Nov. 1999
	55	MCCARTHY, J. 1963. Towards a mathematical science of computation. In Information Processing 1962, 21-28.
	56	R. Milner, Communication and concurrency, Prentice-Hall, Inc., Upper Saddle River, NJ, 1989
	57	MILNER, R. 1991. The polyadic pi-calculus: A tutorial. Tech. Rep. ECS-LFCS-91-180. University of Edinburgh, Edinburgh, Scotland.
	58	MILNER, R. 1992a. Action structures. Tech. Rep. ECS-LFCS-92-249. University of Edinburgh, Edinburgh, Scotland.
	59	MILNER, R. 1992b. Functions as processes. Math. Struct. Comput. Sci. 2, 2, 119-141.
	60	Dave Berry , Robin Milner , David N. Turner, A semantics for ML concurrency primitives, Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.119-129, January 19-22, 1992, Albuquerque, New Mexico, United States [doi>10.1145/143165.143191]
	61	Robin Milner , Joachim Parrow , David Walker, A calculus of mobile processes, I, Information and Computation, v.100 n.1, p.1-40, Sept. 1992 [doi>10.1016/0890-5401(92)90008-4]
	62	Robin Milner , Joachim Parrow , David Walker, Modal logics for mobile processes, Theoretical Computer Science, v.114 n.1, p.149-171, June 14 1993
	63	MONTANARI,U.AND PISTORE, M. 1995. Concurrent semantics for the pi-calculus. Electron. Notes Comput. Sci. 1.
	64	Ugo Montanari , Daniel Yankelevich, A Parametric Approach to Localities, Proceedings of the 19th International Colloquium on Automata, Languages and Programming, p.617-628, July 13-17, 1992
	65	MOSSES, P. D. 1998. Semantics, modularity and rewriting logics. ENTCS 15.
	66	Xavier Nicollin , Joseph Sifakis, An Overview and Synthesis on Timed Process Algebras, Proceedings of the Real-Time: Theory in Practice, REX Workshop, p.526-548, June 03-07, 1991
	67	NIELSEN, M., PLOTKIN,G.,AND WINSKEL, G. 1981. Petri nets, event structures and domains, part 1. Theoret. Comput. Sci.
	68	Chiara Nottegar , Corrado Priami , Pierpaolo Degano, Semantic-Driven Performance Evaluation (Extended Abstract), Proceedings of the Second Internationsl Conference on Fundamental Approaches to Software Engineering, p.204-218, March 22-28, 1999
	69	Chiara Nottegar , Corrado Priami , Pierpaolo Degano, Performance Evaluation of Mobile Processes via Abstract Machines, IEEE Transactions on Software Engineering, v.27 n.10, p.867-889, October 2001 [doi>10.1109/32.962559]
	70	ORAVA, F. 1994. On the formal analysis of telecommunications protocols. Ph.D. dissertation Dept. of Computer Systems, Uppsala University and SICS.
	71	ORAVA,F.AND PARROW, J. 1992. An algebraic verification of a mobile network. Forma. Asp. Comput. 497-543.
	72	David Park, Concurrency and Automata on Infinite Sequences, Proceedings of the 5th GI-Conference on Theoretical Computer Science, p.167-183, March 23-25, 1981
	73	Benjamin C. Pierce , David N. Turner, Pict: a programming language based on the Pi-Calculus, Proof, language, and interaction: essays in honour of Robin Milner, MIT Press, Cambridge, MA, 2000
	74	PLOTKIN, G. 1981. A structural approach to operational semantics. Tech. Rep. DAIMI FN-19. Aarhus University, Aarhus, Denmark.
	75	Vaughan Pratt, Modeling concurrency with partial orders, International Journal of Parallel Programming, v.15 n.1, p.33-71, Feb. 1986 [doi>10.1007/BF01379149]
	76	Vaughn Pratt, Modeling concurrency with geometry, Proceedings of the 18th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.311-322, January 21-23, 1991, Orlando, Florida, United States [doi>10.1145/99583.99625]
	77	PRATT, V. Higher dimensional automata revisited. MFCS. To appear.
	78	PRIAMI, C. 1995. Stochastic pi-calculus. Comput. J. 38, 6, 578-589.
	79	PRIAMI, C. 1996a. Enhanced operational semantics for concurrency. Ph.D. dissertation. Dipartimento di Informatica, Universit` a di Pisa, Pisa, Italy. (Available as Tech. Rep. TD-08/96).
	80	Corrado Priami, Integrating Behavioural and Performance Analysis with Topology Information, Proceedings of the 29th Hawaii International Conference on System Sciences (HICSS'96) Volume 1: Software Technology and Architecture, p.508, January 03-06, 1996
	81	PRIAMI, C. 1996c. Interleaving-based partial ordering semantics. In Proceedings of the Italian Conference on Theoretical Computer Science (Ravello, Italy, Nov.), World Scientific, River Edge, NJ, pp. 264-278.
	82	Corrado Priami , Daniel Yankelevich, Read-Write Causality, Proceedings of the 19th International Symposium on Mathematical Foundations of Computer Science 1994, p.567-576, August 22-26, 1994
	83	RABINOVICH,A.AND TRAKHTENBROT, B. 1988. Nets of processes. Fund. Inf. XI, 4, 357-404.
	84	Wolfgang Reisig, Petri nets: an introduction, Springer-Verlag New York, Inc., New York, NY, 1985
	85	John Hamilton Reppy, Higher-order concurrency, Cornell University, Ithaca, NY, 1992
	86	SANGIORGI, D. 1992. Expressing mobility in process algebras: First-order and higher-order paradigms. Ph.D. dissertation. University of Edinburgh, Edinburgh, Scotland.
	87	Davide Sangiorgi, Locality and True-concurrency in Calculi for Mobile Processes, Proceedings of the International Conference on Theoretical Aspects of Computer Software, p.405-424, April 19-22, 1994
	88	STORRLE, H. 1998. An evaluation of high-end tools for Petri nets. Tech. Rep. Ludwig-Maximilians- Universitat Munchen, Munich, Germany.
	89	THOMSEN, B. 1993. Plain CHOCS: A second genertion calculus for higher order processes. Acta Inf. 30, 1, 1-59.
	90	THOMSEN, B., LETH, L., PRASAD, S., KUO, T.-M., KRAMER, A., KNABE,F.,AND GIACALONE, A. 1993. Facile Antigua release programming guide. Tech. Rep. ECRC-93-20. European Computer-Industry Research Centre.
	91	Rob J. van Glabbeek , Ursula Goltz, Equivalence Notions for Concurrent Systems and Refinement of Actions (Extended Abstract), Proceedings on Mathematical Foundations of Computer Science 1989, p.237-248, August 28-September 01, 1989
	92	Rob J. VanGlabbeek , Scott A. Smolka , Bernhard Steffen, Reactive, generative, and stratified models of probabilistic processes, Information and Computation, v.121 n.1, p.59-80, Aug. 15, 1995 [doi>10.1006/inco.1995.1123]
	93	WALKER, D. 1994. Objects in the pi-calculus. Inf. Comput.
	94	Glynn Winskel, Event Structure Semantics for CCS and Related Languages, Proceedings of the 9th Colloquium on Automata, Languages and Programming, p.561-576, July 12-16, 1982
	95	Glynn Winskel, Petr nets, algebras, morphisms, and compositionality, Information and Computation, v.72 n.3, p.197-238, March 1987 [doi>10.1016/0890-5401(87)90032-0]

CITED BY 16

	Jianwei Niu , Joanne M. Atlee , Nancy A. Day, Composable semantics for model-based notations, Proceedings of the 10th ACM SIGSOFT symposium on Foundations of software engineering, November 18-22, 2002, Charleston, South Carolina, USA
	Corrado Priami, Simulation and verification I: design environments for complex systems, Proceedings of the 35th conference on Winter simulation: driving innovation, December 07-10, 2003, New Orleans, Louisiana
	Fabio Martinelli, Analysis of security protocols as open systems, Theoretical Computer Science, v.290 n.1, p.1057-1106, 1 January 2003
	Yingzhou Zhang , Baowen Xu, A survey of semantic description frameworks for programming languages, ACM SIGPLAN Notices, v.39 n.3, March 2004
	Jianwei Niu , Joanne M. Atlee , Nancy A. Day, Composable semantics for model-based notations, ACM SIGSOFT Software Engineering Notes, v.27 n.6, November 2002
	Chiara Bodei , Pierpaolo Degano , Riccardo Focardi , Corrado Priami, Primitives for authentication in process algebras, Theoretical Computer Science, v.283 n.2, p.271-304, June 14, 2002
	M. Curti , P. Degano , C. Priami , C. T. Baldari, Modelling biochemical pathways through enhanced π-calculus, Theoretical Computer Science, v.325 n.1, p.111-140, 28 September 2004
	Vashti Galpin, A format for semantic equivalence comparison, Theoretical Computer Science, v.309 n.1, p.65-109, 2 December 2003
	C. Bodei , P. Degano , R. Focardi , C. Priami, Authentication primitives for secure protocol specifications, Future Generation Computer Systems, v.21 n.5, p.645-653, May 2005
	Chiara Bodei , Pierpaolo Degano , Corrado Priami, Checking security policies through an enhanced control flow analysis, Journal of Computer Security, v.13 n.1, p.49-85, January 2005
	Roberto Barbuti , Giulio Caravagna , Andrea Maggiolo-Schettini , Paolo Milazzo, An intermediate language for the stochastic simulation of biological systems, Theoretical Computer Science, v.410 n.33-34, p.3085-3109, August, 2009
	MohammadReza Mousavi , Michel A. Reniers , Jan Friso Groote, SOS formats and meta-theory: 20 years after, Theoretical Computer Science, v.373 n.3, p.238-272, April, 2007
	Flemming Nielson , Hanne Riis Nielson , Corrado Priami , Debora Rosa, Control Flow Analysis for BioAmbients, Electronic Notes in Theoretical Computer Science (ENTCS), v.180 n.3, p.65-79, July, 2007
	Roberto Barbuti , Giulio Caravagna , Andrea Maggiolo--Schettini , Paolo Milazzo, An Intermediate Language for the Simulation of Biological Systems, Electronic Notes in Theoretical Computer Science (ENTCS), v.194 n.3, p.19-34, January, 2008
	Johannes Borgström , Andrew D. Gordon , Andrew Phillips, A Chart Semantics for the Pi-Calculus, Electronic Notes in Theoretical Computer Science (ENTCS), v.194 n.2, p.3-29, January, 2008
	Paola Lecca, Simulating the cellular passive transport of glucose using a time-dependent extension of Gillespie algorithm for stochastic π-calculus, International Journal of Data Mining and Bioinformatics, v.1 n.4, p.315-336, April 2007