Title
Software Components: a Formal Semantics Based on Coloured Petri Nets
Abstract
This paper proposes a component model compliant with the current practice of Software Engineering, yet provided with a sound formal semantics based on Coloured Petri nets. Our proposal is structured as follows: 1) Define a component model. We have chosen a component model inspired by the CORBA Component Model (CCM), yet simpler and more precise. 2) Propose a notation to formally specify the internal behaviour of a software component. Our formal approach is based on Coloured Petri nets which makes it well suited to the modelling of concurrent, distributed or event-driven systems, and amenable to formal verification. 3) Define a mapping from the constructs of the component model (facets, receptacles, event sources and sinks) to the constructs of the Petri-net based behavioural specification (e.g. places, transitions, etc.). 4) Provide a formal definition of inter-components communication primitives, (invocation of methods, event-based communication). This definition is also given in terms of Petri nets. 5) Provide a denotational semantics of an assembly of components, in order to define the behaviour of such a system in terms of the individual behaviour of each component and of the formal definition of inter-component communication primitives.
Year
DOI
Venue
2006
10.1016/j.entcs.2006.05.016
Electronic Notes in Theoretical Computer Science
Keywords
Field
DocType
Component models,Coloured Petri Net,Signal Nets
Coloured Petri net,Petri net,Computer science,Denotational semantics,Common Component Architecture,Theoretical computer science,Formal specification,Formal methods,Component-based software engineering,Formal verification
Journal
Volume
ISSN
Citations 
160
1571-0661
11
PageRank 
References 
Authors
0.57
5
2
Name
Order
Citations
PageRank
Remi Bastide1181.75
Eric Barboni228018.82