5th IPM International Conference on
Fundamentals of Software Engineering
(FSEN 2013)
24 - 26 April, 2013
Tehran, Iran



Home

Topics of Interest

Paper Submission

Proceedings

Important Dates

Keynote Speakers

Committees

Programme

Registration

Visa

Travel Info

Guestbook

Contact Us

FSEN Homepage




In cooperation with:





FSEN'05  |  FSEN'07  |  FSEN'09  |  FSEN'11  |  FSEN Homepage

Keynote Speakers


Jose Meseguer - University of Illinois at Urbana-Champaign, USA

Title: Symbolic Formal Methods: Combining the Power of Rewriting, Narrowing, SMT Solving and Model Checking

Abstract: Symbolic techniques that represent possibly infinite sets of states by symbolic constraints and support decision or semi-decision procedures based on such constraints have become essential to automate large parts of the verification effort and make verification much more scalable. They include: (i) SMT solving; (ii) rewriting- and unification-based techniques, including rewriting and narrowing modulo theories; and (iii) automata-based model checking techniques, which describe infinite sets of states and/or system traces symbolically by various kinds of automata. However, a key problem limiting the applicability of current symbolic techniques is lack of, or limited support for, extensibility. That is, although certain classes of systems can be formalized in ways that allow the application of specific symbolic analysis techniques, many other systems of interest fall outside the scope of such techniques. There is a real need to extend and combine the power of symbolic analysis techniques to cover a much wider class of systems. The talk will present some recent advances towards the goal of combined, extensible symbolic formal methods within the context of rewriting logic and Maude.





Wolfgang Reisig - Humboldt-Universität zu Berlin, Germany

Title: Service Oriented Computing: Forthcoming challenges

Abstract: Service-oriented Computing has established itself as a core paradigm of modern software architectures. Nevertheless, some obstacles prevent even more widespread use of service oriented architectures (SOAs). To overcome those obstacles, in particular the following questions have to be addressed:
  1. SOAs are more and more implemented in the cloud. To what extent are the stakeholders affected by this change of technology?
  2. It turned out useful to conceive not only software components, but also humans and technical systems as service providers and service requesters. How can a unified approach to SOA cope with this?
  3. Basic notions such as correctness and equivalence are clear cut and undisputed for classical programs. Are there corresponding generally acceptable and manageable such notions for SOAs?
  4. Quick assignment of needed data, software and hardware to services is inevitable for smoothly running SOAs. How can a small, flexible infrastructure guarantee this kind of elasticity?
Those questions cannot seriously be answered on an intuitive, informal level. It is inevitable to model services in a formal framework, with the decisive properties of the services be represented as properties of their formal models. The above questions are then addressed and faithfully solved in the framework of the formal models. To this end we suggest methods and principles of formally modeling and analyzing SOAs.





Holger Hermanns - Saarland University, Germany

Title: Stochastic, Hybrid and Real-Time Systems: From Foundations To Applications with Modest

Abstract: Our reliance on complex safety-critical or economically vital systems such as networked automation systems or “smart” power grids increases at an everaccelerating pace. The necessity to study the reliability and performance of these systems is evident, but purely functional models and properties are insufficient in many cases. This has led to the development of integrative approaches that combine probabilities, real-time aspects and continuous dynamics with formal verification.
Today, formal quantitative modelling and analysis is supported by a wide range of tools and formalisms such as Prism with probabilistic guarded commands, Uppaal for graphical modelling and verication of timed automata, or hybrid system model checkers like Phaver. This variety of different languages and tools, however, is a major obstacle for new users seeking to apply formal methods in their field of work.
To overcome these problems, the Modest [4,6] modelling language and its underlying semantic model of stochastic hybrid automata (SHA) have been designed as an overarching formalism of which many well-known and extensively studied models such as Markov decision processes, probabilistic timed systems or hybrid automata are special cases. The construction and analysis of SHA models is supported by the Modest Toolset [1], which supports analysis with a range of different methods. At the current stage, the following analysis components are available: prohver [6] handles probabilistic safety properties for SHA; mcpta performs model checking of probabilistic timed automata using Prism; mctau [2] connects to Uppaal for model checking of timed automata, for which it is more efficient than mcpta; and modes [3] performs statistical model checking and simulation of stochastic timed automata with an emphasis on the sound handling of nondeterministic models.
The Modest Toolset has been used for a variety of applications with different levels of complexity and of expressiveness. These include really cool safety critical hard real-time wireless control applications for bicycles [5] as well as high-speed trains [6], and innovative electric power grid control strategies [7]. The applications combine different abstraction and analysis techniques supported by the Modest Toolset.

References
  1. The Modest Toolset website, www.modestchecker.net.
  2. Jonathan Bogdoll, Alexandre David, Arnd Hartmanns, and Holger Hermanns. mctau: Bridging the gap between Modest and UPPAAL. In SPIN, volume 7385 of LNCS, pages 227–233. Springer, 2012.
  3. Jonathan Bogdoll, Arnd Hartmanns, and Holger Hermanns. Simulation and statistical model checking for Modestly nondeterministic models. In MMB/DFT, volume 7201 of LNCS, pages 249–252. Springer, 2012.
  4. H. C. Bohnenkamp, P. R. D’Argenio, H. Hermanns, and J.-P. Katoen. MoDeST: A compositional modeling formalism for hard and softly timed systems. IEEE Transactions on Software Engineering, 32(10):812–830, 2006.
  5. Hernan Baro Graf, Holger Hermanns, Juhi Kulshrestha, Jens Peter, Anjo Vahldiek, and Aravind Vasudevan. A verified wireless safety critical hard real-time design. In WOWMOM, pages 1–9. IEEE, 2011.
  6. Ernst Moritz Hahn, Arnd Hartmanns, Holger Hermanns, and Joost-Pieter Katoen. A compositional modelling and analysis framework for stochastic hybrid systems. Formal Methods in System Design, 2012.
  7. Arnd Hartmanns, Holger Hermanns, and Pascal Berrang. A comparative analysis of decentralized power grid stabilization strategies. In Winter Simulation Conference, 2012.
© 2012 Copyright, School of Computer Science, IPM