Transcript ppt

WSMX Execution Semantics
Executable Software Specification
Eyal Oren
DERI
[email protected]
Background information
• WSMX: execution environment for dynamic
discovery, selection, mediation and invocation
of semantic web services
• WSMX is built on WSMO: services, ontologies,
goals and mediators
• WSMX: manages repository, achieves user’s goal
by selecting matching service, mediating and
invoking
[email protected]
WSMX execution semantics
2
Designing WSMX
• Conceptual model: what are we talking about
• Architecture: components, how they interact
• Execution semantics: system behaviour
goal
manager
web service
web service
discovery
selection
mediation
invocation
web service
repository
[email protected]
WSMX execution semantics
web service
3
What did we do?
• Design of WSMX includes formal specification of
system behaviour
• Reasons:
– enlarging developers’ understanding of the system
– proving properties of the system
– enabling model-driven component execution
• We present the execution semantics of WSMX
• Did our approach address the objectives?
[email protected]
WSMX execution semantics
4
What are execution semantics?
• Four phases in software development:
requirements, design, implementation, testing
• Formal methods can be used during design: to
improve the design process and the result
• Formal method: a mathematically-based
language for specifying systems
• Execution semantics: a formal definition of
operational behaviour of a system.
[email protected]
WSMX execution semantics
5
Why model execution semantics?
• Formal methods do not make correct
programs!
• Increase understanding and agreement
between project members (by explicit
specification process)
• To check properties of the constructed
specification: discover future properties of the
modelled system
[email protected]
WSMX execution semantics
6
Why model execution semantics?
• Execute the specification
– general idea: specification is input for execution
engine; engine executes model, informs components
to perform a task (workflow management, business
process management)
– main argument in favour: flexibility, not hardcoding this interplay, no need to translate
specification into programming code
– main argument against: inefficient implementation;
might not be important: if composition is simple and
components themselves are implemented efficiently
[email protected]
WSMX execution semantics
7
Requirements
• Enlarge developers’ understanding: technique
must be easily readable yet unambiguous
• Check properties of the system: technique must
be formal and have a proof system
• Automate coordination between components:
technique must have operationalisation, and
execution procedure for a model
[email protected]
WSMX execution semantics
8
How to model execution semantics?
• We want to automate control flow between
components
• Components treated as black-boxes: we know
their functionality but not how they operate
• Using Petri nets
– graphical, supposedly easily understood
– formalised, well analysable
– executable
[email protected]
WSMX execution semantics
9
WSMX execution semantics
(see paper)
goal
manager
web service
web service
discovery
selection
mediation
invocation
web service
repository
[email protected]
web service
WSMX execution semantics
10
Using execution semantics
• The goal was:
– understandability
– model checking
– model-driven execution
• Did this work?
[email protected]
WSMX execution semantics
11
Did it work?
• Understandability
– not easily readable: syntax is very simple, but model
gets complex
– hard to write and time-consuming to maintain
– simulation is very helpful
• Executing specification
– technical problems:
synchronous invocation from the engine
– work in progress – the general idea is ok
[email protected]
WSMX execution semantics
12
Did it work?
• Model checking
– large amount of work on problems in Petri nets
(algorithms, tools, decidability & complexity results)
– however, we did not use this possibility:
– during implementation developers had to manually
translate the Petri net specification into Java code.
– but model is not easily readable: implementation did
not strictly follow model!
– model checking not very useful
[email protected]
WSMX execution semantics
13
Conclusion
• Specifying execution semantics as part of software
development
• Three objectives: understandability, model checking,
component execution
• Used Petri nets to specify the behaviour of WSMX
• Petri nets are not a useful technique for this
specification:
– not easily readable (and not easily writable)
– model checking and executability in principle possible
[email protected]
WSMX execution semantics
14
Future
• Investigate other techniques that overcome these
problems
– take into account: we want to do model checking and execute
the specification
– UML Activity diagrams: easily readable, more intuitive, no
model execution
– YAWL: builds on Petri nets, designed for usability, no good tools
yet
• Separate techniques:
– use one model for proving and executing
– use second model for clarification and understanding
– (second would be generated from the first)
[email protected]
WSMX execution semantics
15
Questions?
[email protected]
WSMX execution semantics
16