Workshops Dates: 27-28 August 2012

5th International Workshop UML&FM 2012

Organized by Isabelle Perseil, INSERM et LTCI (Telecom Paris Tech)

Many interest groups from a research perspective are in favour of the creation of this workshop. For more than a decade now, the two communities of UML and formal methods have been working together to produce a simultaneously practical (via UML) and rigorous (via formal methods) approach to software engineering. UML is the de facto standard for modelling various aspects of software systems in both industry and academia, despite the inconvenience that its current specification is complex and its syntax imprecise. The fact that the UML semantics is too informal have led many researchers to formalize it with all kinds of existing formal languages, like OCL, Z, B, CSP, VDM, Petri Nets, UPPAAL, HOL, Coq, PVS etc. This fifth edition of the workshop will be open to various subjects as the main objective is to encourage new initiatives of building bridges between informal, semi-formal and formal notations.The workshop seeks contributions from researchers and practitioners interested in all aspects of integrating UML and formal methods.

UML&FM'2012 Program

more info at http://www-public.int-evry.fr/~gibson/Workshops/UML-FM-2012.html

6th International Workshop on Verification and Evaluation of Computer and Communication Systems (VECoS 2012)

Organized by Nejib Ben Hadj Alouane , Oasis-ENIT Tunisie and Patrice Moreaux Listic - Polytech Annecy-Chambéry France

The aim of VECoS workshop is to bring together researchers and practitioners, in the areas of Verification, Control, Performance, Quality of service, Dependability evaluation and Assessment, to discuss the state of the art for solving the challenges facing us today in various modern computer and communication systems in which functional and extra functional properties are strongly interrelated. Thus, the main motivation for VECoS is to encourage the cross-fertilization between formal verification and evaluation approaches, methods and techniques especially those based on the specification formalisms for concurrent, distributed and soft/hard systems.

VECoS 2012 Program

more info at http://vecos-world.org

2nd Workshop on Formal Methods in the Development of Software (WS-FMDS 2012)

Organized by César Andrés and Luis Llana, Universidad Complutense de Madrid

Developing software concerns all the aspects of the production cycle of software systems and requires expertise in data management, design and algorithm paradigms, programming languages, and human computer interfaces. Most software development life cycle methodologies are either iterative or follow a sequential model. Such systems may contain a huge amount of lines of code. Thus, when developing these systems, it is necessary to apply sound engineering principles in order to economically obtain reliable and efficient software. The aim of WS-FMDS 2012 is to provide a forum for researchers who are interested in the application of formal methods on systems which are being developing with a software methodology. In particular, this workshop is intended to bring together scientists and practitioners who are active in the area of formal methods and interested in exchanging their experiences in the industrial usage of these methods. This workshop also strive to promote research and development for the improvement of formal methods and tools for industrial applications.

WS-FMDS 2012 Program

more info at http://antares.sip.ucm.es/ws-fmds2012/

17th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2012)

Organized by Ralf Pinger, Mobility and Logistics Division Rail Automation Siemens AG Germany and Marielle Stoelinga, Formal Methods & Tools * University of Twente * The Netherlands

The aim of the FMICS workshop series is to provide a forum for researchers who are interested in the development and application of formal methods in industry. In particular, FMICS brings together scientists and engineers that are active in the area of formal methods and interested in exchanging their experiences in the industrial usage of these methods. The FMICS workshop series also strives to promote research and development for the improvement of formal methods and tools for industrial applications.

FMICS 2012 Program

more info at http://fmt.cs.utwente.nl/conferences/fmics2012/

International Workshop TLA 2012

Organized by Leslie Lamport, Microsoft Research Mountain View, Stephan Merz, INRIA Nancy & LORIA

TLA+ is a formal language for specifying systems that is seeing some use in industry. The TLA 2012 workshop is a forum for practitioners and researchers interested in the use of the TLA+ specification language and its associated tools. Presentations of academic or industrial developments based on TLA+ or PlusCal, of extensions of the existing TLA+ tools or of the innovative use of these tools are of particular interest, as are contributions concerning the integration of TLA+ with other system engineering techniques, reports on using TLA+ in teaching, and any other topic clearly related to the TLA+ language or tools. Presentation of ongoing work is specifically encouraged.

TLA+ Program

more info at http://tla2012.loria.fr/

14th International Workshop Infinity 2012

Organized by Mohamed Faouzi Atig, Uppsala University and Ahmed Rezine , Linköping University, Sweden

The aim of the INFINITY workshop is to provide a forum for researchers interested in the development of formal methods and algorithmictechniques for the analysis of systems with infinitely many states, and their application in automated verification of complex software and hardware systems. Topics of interest include (but are not limited to): infinite-statemodels of software/hardware systems; abstraction techniques for infinite-statesystems; symbolic analysis techniques and data structures for representing infinite state spaces; model-checking, static analysis, abstract interpretation, preorder/equivalence-checking, and control synthesis for infinite-statesystems; parameterized networks of parallel processes, dynamic networks, mobile systems; systems with unbounded dynamic data and control structures; probabilistic and timed systems; games in modeling and verification ofinfinite-state systems; verification techniques for security properties, cryptographic protocols, systems biology.

INFINITY Program

more info at http://www.it.uu.se/workshop/infinity2012/

10th International Workshop Overture/VDM

Organized by Nico Plat West Consulting, the Netherlands and Claus Ballegard Nielsen, Aaurus University, Denmark and Steve Riddle, Newcastle University, UK

The proposed workshop will emphasise topics that mesh closely with the themes of FM 2012 itself, particularly application experience in industry, validation of tools and methods and the development of tools. The aim of the workshop is to identify and encourage new collaborative research, and to foster current strands of work towards publication in the mainstream conferences and journals. Proceedings will therefore be issued as a technical report and online, but we do not plan separate proceedings volume in LNCS or a special journal issue unless the quality of the papers is subsequently seen to merit it.

VDM 2012 Program

more info at http://wiki.overturetool.org/index.php/10th_Overture_Workshop

1st Workshop on Quantities in Formal Methods (QFM 2012)

Organizers: Axel Legay and Uli Fahrenberg, Irisa / INRIA Rennes, France, Claus Thrane, Aalborg U, Denmark

This workshop will focus on quantities in modeling, verification, and synthesis. Modern applications of formal methods require to reason formally on quantities such as time, resources, or probabilities. Standard formal methods and tools have gotten very good at modeling (and verifying) qualitative properties: whether or not certain events will occur. During the last years, these methods and tools have been extended to also cover quantitative aspects, notably leading to tools like e.g. UPPAAL (for real-time systems), PRISM (for probabilistic systems), and PHAVer (for hybrid systems). A lot of work remains to be done however before these tools can be used in the industrial applications at which they are aiming. Particular issues are as follows:
- Almost all current methods and tools are not robust, in the sense that small changes in the quantitative inputs (e.g. due to measurement errors) can lead to large changes in the verification result. This is not desirable, and fixing it requires a paradigm switch away from the Boolean verification domain to real-valued domains.
- Most currently used algorithms for quantitative verification (and synthesis) are not efficient enough and do not scale well for industrial-size systems. New approaches, such as e.g. simulation-based statistical model checking, seem promising in this regard; but it is an open question how to apply them to synthesis.
- Almost all current methods and tools focus on only one quantitative aspect: either time, or resources, or probabilities. Integration of these formalisms is an active research area.

more info at http://qfm2012.cs.aau.dk/