Keynote Speakers


Prof Mike Hinchey
(Lero, Ireland)
Mike Hinchey is Scientific Director of Lero-the Irish Software Engineering Research Centre and Professor of Software Engineering at University of Limerick. He holds a BSc in Computer Science from University of Limerick, an MSc in Computation from University of Oxford and a PhD in Computer Science from University of Cambridge. For several years he was Director of the NASA Software Engineering Laboratory and continues to serve as a NASA expert. In 2008, he received a NASA Honor Award and in 2009 he received the NASA James Kerley Award for innovation.

Click here for the abstract of Prof. Hinchey's keynote speech.



Prof Wolfgang Reisig
(Humboldt-Universitat zu Berlin, Germany)
Wolfgang Reisig is a professor at the Computer Science Institute of Humboldt-Universitaet zu Berlin, Germany since 1993. He studied Physics and Computer Science in Karlsruhe and Bonn, where he graduated with a masters degree in 1974. Prof. Reisig was a senior research at the International Computer Science Institute (ICSI) in Berkeley, California in 1997, and got the "Lady Davis Visiting Professorship" at the Technion, Haifa (Israel) in 2000/2001. In the years 2002 and 2005 he received an IBM Faculty Award for his contribution to Cross-organizational Business Processes and the Analysis of Service Models. In 2006, he had the Beta Chair of Technical University of Eindhoven. Prof. Reisig is a member of the European Academy of Sciences, Academia Europaea.

Click here for the abstract of Prof. Hinchey's keynote speech.



KEYNOTE SPEAKERS OF PREVIOUS SEEFM WORKSHOPS


Prof Jonathan Bowen
(London South Bank University, UK)
SEEFM'05


Prof John Derrick
(Sheffield University, UK)
SEEFM'05



Prof Mike Holcombe
(Sheffield University, UK)
SEEFM'03



Prof Marco Pistore
(Institute for Scientific and Technological Research, Italy)
SEEFM'07



Prof Martin Wirsing
(Ludwig-Maximilians University of Munich, Germany)
SEEFM'07


SEEFM'09 KEYNOTE SPEECHES

Prof. Mike Hinchey
Formally Specifying Autonomous and Agent-Based NASA Space Exploration Missions

NASA plans innovative and novel approaches to future (unmanned) space exploration missions. Future missions involve sending spacecraft and robots to harsh environments, where resilience is necessary for the survival of the mission. In addition, distances and communication lead times between the spacecraft and Earth, necessitate much of the mission operation being autonomous.

We have been conducting research on using agent-based concepts and in developing autonomous systems based on Autonomic Computing, whereby the mission is embued with self-management capabilities. The need for assurance that decisions, etc., taken by the mission are within the remit of the mission and will ensure its surviveability is of growing importance.

We describe the PAM (Prospecting Asteroid Mission) sub-mission of the ANTS (Autonomous Nano Technology Swarm) concept mission, which illustrates the issues that may potentially arise in future swarm-based missions. We describe our approach to formally specifying ANTS and other missions, as well as efforts to apply agent-oriented software engineering and formal methods in a combined framework.

Prof. Wolfgang Reisig
Deciding Properties of Services

Service orientation is a promising architectural concept to quickly and cost effectively compose encapsulated software components ("services"), and to adapt them to new requirements. Service orientation has evolved from very pragmatic problems and backgrounds. Little attention has been directed to theoretical and conceptual problems of the area.

Central in the context of Service-oriented computing is the notion of a partner service P for a given service, S. The service S communicates with P by means of asynchronous communication.

One is usually interested in partners P for a given service S, such that P meets particular requirements. Typical examples are partners that avoid deadlocks or lifelocks, or that reach terminal states. Formulated more generally, we are interested in partners of S that guarantee particular properties, p. Typical examples include:

  • Does the partner P guarantee property p?
  • How characterize all partners with property p?
  • Does the set of partners with property p exhibit a particular structure (e.g. an order)?
  • Is there a canonical ("most interesting") partner with property p?
  • Which kind of equivalence does property p imply?

We discuss the conceptual basis to formulate and to answer this kind of questions. It turns out that the behaviour of composted services can be represented in terms of (in general infinite) trees of reachable states and steps, with branching states denoting alternatives. Elementary operations on such trees suffice to characterize the above questions. Furthermore, "regular" infinite trees can be represented as finite graphs. This yields decision procedures for the questions.



SEEFM'09
4th South-East European Workshop on Formal Methods
"Formal Methods for Web Services", and
"Formal Methods for Agent-based Systems"
City College (www.city.academic.gr)
South-East European Research Centre SEERC (www.seerc.org)
Thessaloniki, Greece, 4-5 December 2009