A satellite workshop of FM2016
General theme of the workshop: “Formal Integrated Development Environment (F-IDE)
for joint construction of an application and its correctness proof upon its formalized specification”.
High levels of safety, security and also privacy standards require the use of formal methods to specify and develop compliant software (sub)systems. Any standard comes with an assessment process, which requires a complete documentation of the application in order to ease the justification of design choices and the review of code and proofs.
Ideally, an F-IDE dedicated to such developments should comply with several requirements. The first one is to associate a logical theory with a programming language, in a way that facilitates the tightly coupled handling of specification properties and program constructs. The second one is to offer a language/environment simple enough to be usable by most developers, even if they are not fully acquainted with higher-order logics or set theory, in particular by making development of proofs as easy as possible. The third one is to offer automated management of application documentation. It may also be expected that developments done with such an F-IDE are reusable and modular. Moreover, tools for testing and static analysis may be embedded in this F-IDE, to help address most steps of the assessment process.
Last year's F-IDE workshop was a satellite event of FM 2015, in June 2015 in Oslo, Norway. The workshop was attended by ~25 participants, and the programme included 10 presentations (7 research papers, and 3 tool demos) and an invited talk given by John Fitzgerald from Newcastle University, UK, on integrated tool chains to support rigorous system design. Post-proceedings have been edited as EPTCS proceedings (EPTCS 187).
The workshop is opened to contributions on all aspects of a system development process, including specification, design, implementation, analysis and documentation. It should allow the presentation of tools, methods, techniques and experiments. Topics of interest include, but are not limited to, the following:
9:05-10:00 Keynote - Kim G. Larsen (Aalborg University, Denmark)
Timed automata and games, priced timed automata and energy automata have emerged as useful formalisms for modeling real-time and energy-aware systems as found in several embedded and cyber-physical systems. In this talk we will survey how the various component of the UPPAAL tool-suite over a 20 year period has been developed to support various type of analysis of these formalisms. This includes the classical usage of UPPAAL as an efficient model checker of hard real time constraints of timed automata models, but also the branch UPPAAL CORA which have been extensively used to find optimal solutions to time-constrained scheduling problems. More ambitiously, UPPAAL TIGA allows for automatic synthesis of strategies – and subsequent executable control programs – for safety and reachability objectives. Most recently the branch UPPAAL SMC offers a highly scalable statistical model checking engine supporting performance analysis of stochastic hybrid automata, and the branch UPPAAL STRATEGO which supports synthesis (using machine learning) of near-optimal strategies for stochastic priced timed games. The keynote will review the various branches of UPPAAL and highlight their concerted applications to a selection of real-time and cyber-physical examples.