Formal Specification
Definitions
Term: Formal Specification |
Domain: Cross-cutting issues | ||||
---|---|---|---|---|---|
Engineering and Design (KM-ED) |
Adaptation and Monitoring (KM-AM) |
Quality Definition, Negotiation and
Assurance (KM-QA) |
Generic (domain independent) |
||
D o m a i n : L a y e r s |
Business Process Management (KM-BPM) |
A formal model of the key functional and non-functional properties of a Web service. [PO-JRA-2.2.1] | A formal model that describes relevant aspects of Web service behavior during execution, monitoring events, adaptation and coordination requirements. [PO-JRA-2.2.1] | (1) A formal model of required and actual quality attributes of a service. (2) A formal model of quality contracts (agreements), negotiation rules, protocols, compensations and negotiating behavior patterns. [PO-JRA-1.3.1] | |
Service Composition and
Coordination (KM-SC) |
A formal model of service composition expressed and analyzed using an appropriate formalism, such as Petri-nets, timed automatons, pi-calculus, or (XML) types for data exchanged between services. [PO-JRA-2.2.1] | A formal model that expresses a spectrum of potential modifications of a composition (e.g. distributed enactment, fragmentation, merging, or rebinding), coordination mechanisms between parts of a composition, and actual changes in a composition (e.g. change algebra). [PO-JRA-2.2.1] | A formal model that expresses aggregation of QoS characteristics across components of a service composition. [PO-JRA-1.3.1] | ||
Service Infrastructure (KM-SI) |
A formal description of roles and relationships between elements of service infrastructure and the adaptation mechanisms. [PO-JRA-2.1.1] [CD-JRA-2.3.4] | A formal model of relationship between the designed / expected / empirically measured run-time parameters of the service infrastructure layer and the overall QoS characteristic of a service. [PO-JRA-2.2.2] [CD-JRA-2.3.4] | |||
Generic (domain independent) |
A formal specification is a precise mathematical description, supported by a sound logic and reasoning apparatus, of what a system should do in terms of its capabilities and the functionality offered. [PO-JRA-2.2.1] |
Competencies
-
UniDue: Requirements Engineering; http://www.sse.uni-due.de/wms/en/index.php?go=110; Klaus Pohl, Andreas Gehlert
-
UniDue: Software Architecture; http://www.sse.uni-due.de/wms/en/?go=108; Klaus Pohl, Andreas Metzger, Kim Lauenroth
-
UniDue: Quality Assurance; http://www.sse.uni-due.de/wms/en/?go=111; Klaus Pohl, Andreas Metzger, Osama Sammodi, Eric Schmieders
- POLIMI: Adaptive Web Services; http://home.dei.polimi.it/pernici/ws-research.html; Barbara Pernici, Maria Grazia Fugini, Danilo Ardagna, Pierluigi Plebani, Cinzia Cappiello, Marco Comuzzi, Kyriakos Kritikos
- UOC: Service Oriented Computing; http://www.ics.forth.gr/isl/r-d-activities/soc.html; Dimitris Plexousakis, George Baryannis, Kyriakos Kritikos
- Tilburg: Service Design & Modeling Methodologies; http://www.tilburguniversity.nl/eriss/research/;
Vasilios Andrikopoulos, Mike Papazoglou, Michael Parkin
- UPM: Formal Methods; http://clip.dia.fi.upm.es; Manuel
Carro, Ángel Herranz, Julio Mariño
- UCBL:
Formel Methods; http://liris.cnrs.fr/bd/; Mohsen
Rouached, Salima Benbernou
- SZTAKI: Formal Methods; http://www.lpds.sztaki.hu ; Zsolt Nemeth
Scenarios
TBD
References
- [PO-JRA-2.1.1]
"Survey on Business Process Management"
- [PO-JRA-2.2.1] "Overview of the State of the Art in Composition and Coordination of Services"
- [PO-JRA-2.2.2] "Models and Mechanisms for Coordinated Service Compositions"
- [CD-JRA-2.3.4] "Decision support for local adaptation"
- [PO-JRA-1.3.1]
"Survey of Quality Related Aspects Relevant for Service-based
Applications"