Tracks

• Bioscientific Data Processing and Modeling
  Organizers: Joost Kok (NL), Anna-Lena Lamprecht (D), Fons Verbeek (NL), Mark Wilkinson (CAN)
  
  
• Learning Techniques for Software Verification and Validation
  Organizers: Ed Clarke (Carnegie Mellon University), Mihaela Bobaru (JPL), Corina Pasareanu (Carnegie Mellon/NASA Ames), Dawn Song (UC Berkeley)
  
  
• Model-Based Testing and Model Inference
  Organizers: Karl Meinke (S), Neil Walkinshaw (GB)
  
  
• Quantitative Modelling and Analysis
  Organizers: Joost-Pieter Katoen (D)
  
  
• Software Aspects of Robotic Systems
  Organizers: Jens Knoop (TU Vienna, A), Dietmar Schreiner ( TU Vienna, A)
  
  
• Runtime Verification: the application perspective
  Organizers: Lenore Zuck (USA), Ylies Falcone (F)
  
  
• Technologies for Mastering Change
  Organizers: Ina Schaefer (D), Martin Leucker (D), Malte Lochau (D)
  
  
• Timing Constraints: Theory Meets Practice
  Organizers: Johan Nordlander (S)
  
  
• Adaptable and Evolving Software for Eternal Systems
  Organizers: Reiner Hähnle (TU Darmstadt) and Ina Schaefer (TU Braunschweig)
  
  
• LearnLib Tutorial: From finite automata to register interface programs
  
  
• The ITSy Day 2012
  
  
• Process-oriented geoinformation systems and applications
  Organizers: Hartmut Asche (Potsdam University, D)
  
  
• Handling heterogeneity in formal developments of hardware and software systems
  Organizers: Yamine Ait-Ameur (F), Dominique Mery (F)
  
  
• Formal Methods for Intelligent Transportation Systems (CFP)
  Organizers: Alessandro Fantechi (DSI - Univ. of Florence), Francesco Flammini (Ansaldo STS), Stefania Gnesi (ISTI - CNR - Pisa)
  
  

Bioscientific Data Processing and Modeling

This ISoLA 2012 special track focuses at the various topics concerned with the discovery and preservation of knowledge in the biosciences. We invite researchers and practitioners from different application areas to present and discuss theories, methods and technologies for dealing with biological data and models.

Topics of interest include (but are not limited to):

• scientific data management
• data mining
• data stewardship and conservation
• imaging, high-throughput systems
• high performance computing and storage
• modeling and simulation
• visualization and visual analytics

Track Organizers

Joost Kok (NL), Anna-Lena Lamprecht (D), Fons Verbeek (NL), Mark Wilkinson (CAN)

Learning Techniques for Software Verification and Validation

Learning techniques are used increasingly to improve software verification and validation activities. For example, automata learning techniques have been used for extracting behavioral models of software systems. These models can serve as formal documentation of the software and they can be verified using automated tools or used for model-based testing. Automata learning techniques have also been used for automating compositional verification and for building abstractions of software behavior in the context of symbolic or parameterized model checking. Furthermore, automata learning techniques have been used for the automatic inference and security analysis of botnet protocols or in classifying data in black box testing.

This Special Track aims at bringing together researchers and practitioners working on the integration of learning techniques in verification and validation activities for software systems. The Special Track will be part of the 2012 ISoLA International Symposium on Leveraging Applications of Formal Methods, Verification, and Validation.

Topics of interest include (and are not limited to) learning techniques in the context of:

• Synthesis of Behavioral Models for Software
• Automated Compositional Verification
• Security
• Requirements Elicitation and Analysis
• Automated Testing
• Abstraction, Symbolic and Parameterized Verification Techniques
• Improving Practical Applications in Avionics, Telecommunications, etc.

Track Organizers

Ed Clarke (Carnegie Mellon University), Mihaela Bobaru (JPL), Corina Pasareanu (Carnegie Mellon/NASA Ames), Dawn Song (UC Berkeley)

Model-Based Testing and Model Inference

Model-based testing is a recent and successful approach to the problem of automated test case generation. It is particularly useful for testing embedded and reactive software systems that can be modeled by some sort of finite state machine description. In this case, both specification based black-box testing and structural glass box testing can be achieved by model checking automata models against temporal logic formulas. Such formulas can directly describe the  test requirements. Using the counterexample construction facility available in many model checkers, one can then automatically generate abstract test cases that meet the test requirement.

Very recently, several researchers have begun to consider the use of automata learning algorithms for model inference (aka. model mining). These algorithms can be combined with testing procedures such as model-based testing in a variety of ways. In this case they lead to very efficient automated test case generation (ATCG) procedures that can perform better than random testing and other competitive methods. Model inference is also of interest in its own right, as an approach to systems documentation, round-trip engineering, and even as a coverage model for black-box testing.

This track aims to explore the current interactions  between these two fields, and future research directions. Leading researchers in these topics will discuss their approaches. Emerging topics include the problems of learning, model checking and testing infinite state systems, as well as scalability to real world systems and complex data types.

Track Organizers

Karl Meinke (S), Neil Walkinshaw (GB)

Quantitative Modelling and Analysis

Quantitative aspects are manifold. Timing aspects, energy usage, failure rates, resource contention are prominent in embedded and cyber-physical systems.  This session's aim is to provide insight in the current state- of-the art in formal modeling and analysis of quantitative system aspects. This includes recent major tool advancements, techniques that allow for either the analysis of larger classes of models or new properties, case studies showing the potential of tools and algorithms, and so forth. The session focusses on a wide class of application areas ranging from WCET, reliability, performance and dependability analysis to fields as systems biology, optimization, and security.

Track Organizers

Joost-Pieter Katoen (D)

Software Aspects of Robotic Systems

The development of autonomous robotic systems has experienced a remarkable boost within the last years. Away from stationary manufacturing units, current robots have grown up into autonomous, mobile systems that not only interact with real world environments, but also fulfill mission critical tasks in collaboration with human individuals on a reliable basis. Typical fields of application are unmanned vehicles for exploration but also for transportation, reconnaissance and search-and-rescue in hazardous environments, and ambient assisted living for elderly or disabled people.

Hence, algorithms in cognition, computer vision, and locomotion have become hot-spots of research and development. In addition, modern concepts like evolutionary and bio-inspired design have entered the stage to tackle open issues in robotics and to cope with domain specific properties like inherent indeterminism.

The back-side of this boost is an even larger increase in complexity of modern robotic systems. Numerous actuators and sensors have to be controlled simultaneously. Complex actions have to be performed via timed parallel execution of multiple instruction streams on distinct electronic control units. Autonomy, especially long term autonomy as required by deep-sea or space exploration missions, necessitates features of fault-tolerance, error recovery, or at least well-defined fallbacks. Due to the physical interaction of robots with the real world, safety violations are extremely harmful, in the worst-case they might lead to severe damage and even to casualties.

The goal of this track is to bring together researchers and practitioners who are interested in the software aspect of robotic systems. Topics of interest for the track include (but are not limited to): robot programming, languages and compilation techniques, real-time and fault tolerance, dependability, software architectures, computer vision, cognitive robotics, multi-robot-coordination, simulation, bio-inspired algorithms, machine-learning. It continues the 1st International ISoLA Workshop on Software Aspects of Robotic Systems that has been held in Vienna in October 2011,

Authors are invited to submit original, unpublished papers on basic as much as applied research, which are not being considered in another forum. All submitted papers will be carefully evaluated based on originality, significance, technical soundness, and clarity of expression. All submissions must be in English. Submissions should be in PDF format and must not exceed 15 pages in the final camera-ready format.

Track Organizers

Jens Knoop (TU Vienna, A), Dietmar Schreiner ( TU Vienna, A)

Runtime Verification: the application perspective

In the past decade Runtime Verification (RV) has gained much focus, from both research community and practitioners. Roughly speaking, RV combines a set of theories, techniques and tools aiming towards efficient analysis of systems' executions and guaranteeing their correctness using monitoring techniques. One of the major challenges in RV is characterizing and formally expressing requirements that can be monitored.

With the major strides made in recent years, much effort is still needed to make RV an attractive and viable methodology for industrial use. In addition to industry, numerous other domains, such as security, bio-health monitoring, etc., can gain from RV.

The purpose of the "Runtime Verification: the application perspective" track at ISoLA'12 is to bring together experts on runtime verification and potential application domains to try and advance the state-of-the-art on how to make RV more useable and attractive to industry and other disciplines.

Track Organizers

Lenore Zuck (USA), Ylies Falcone (F)

Technologies for Mastering Change

Modern software systems are highly configurable and exist in many different variants in order to operate different application contexts. Furthermore, software systems have to evolve over time in order to deal with changing requirements. Additionally, modern software systems are designed to dynamically adapt their internal structure and behavior at runtime dependent on their environment in order to efficiently use the available resources, such as energy or computing power. These three dimensions of change increase design complexity and also the complexity of the implementation. Hence, they pose new challenges for system validation and verification in order to rigorously an efficiently ensure critical system qualities. The goal of this track is to bring together researchers and practitioners working on the area of verification and validation for diverse software systems covering all three dimensions of change. We aim at identifying and discussing synergies between the existing approaches to develop uniform techniques tackling the challenges of change.

Track Organizers

Ina Schaefer (D), Martin Leucker (D), Malte Lochau (D)

Timing Constraints: Theory Meets Practice

Many embedded systems have timing requirements which must be dealt with throughout the system development process: from the initial timing requirements expressed at an abstract level, through the increasingly concrete layers, to the final implementation level. There is a growing awareness that this process needs support from languages, tools, and methodologies.

The term "timing constraint" encompasses timing requirements, which describe how a system should behave, and timing properties, which describe how the system really behaves. Languages for defining timing constraints allow checking the consistency of specifications and verifying the correctness of implementations with respect to requirements, by both formal means and testing. The AUTOSAR timing extensions provide an example of a domain-specific timing constraint language for automotive systems, but general principles for how to design suitable timing constraint languages are sorely needed.

This track aims to bring together researchers and practitioners who are interested in all aspects of timing constraint languages, including their syntactic and semantic formulation, probabilistic or weakly-hard variants, industrial case studies using timing constraints, tools and methods for verification of properties expressed in timing constraint languages, and methodologies for the use of such languages and tools in the system development process.

Track Organizers

Johan Nordlander (S)

EternalS Session

For this track we invited a number of researchers to present their approaches to tackle the challenge of software evolution in very long-lived systems. The invited format ensures broad coverage of this important topic: diverse solution approaches (language-based, verification-based, process-based), diverse methodologies (learning, modeling, formal verification), as well as diverse application areas (productline engineering, compatibility checking, regression testing) are featured in the six contributions of this half-day track. All of the papers represent systematic rather than ad-hoc proposals which makes them interesting for a wide audience. Together, the papers in this track provide a comprehensive and up-to-date overview of the research community's response to the challenge of evolving software.

Track Organizers

Reiner Hähnle (TU Darmstadt) and Ina Schaefer (TU Braunschweig)

Process-oriented geoinformation systems and applications

It is a well-accepted truism that the vast majority of digital data have a geographical reference. In the past decades geodata have been processed and visualised by dedicated software products of the geoinformation systems (GIS) type for a limited range of scientific and professional applications. However, For more than a deacade, however, both geodata and GIS functionalities are having an increasing, by now almost ubiquitious impact on various fields of everyday life. Against this background space-related, process-orientend software environments will play a decisive role in the development and delivery of a variety of geoinformation and geovisualisation products and services for a wide range of scientific and practical applications alike. This track aims at providing an update on current as well as emerging issues and applications in ubiquitious geoininformation and geovisualisation.

Track Organizers

Hartmut Asche (Potsdam University, D)

Handling heterogeneity in formal developments of hardware and software systems

Nowadays, the formal development of hardware and/or software systems implies the design of several models on which properties are expressed and then formally verified. This development process leads to heterogeneous developments. Heterogeneity may appear in two different forms. The first one is related to the large variety of formal development techniques and to the semantics and proof systems carried out by these techniques. Several formal descriptions may be associated to a given system with different semantics. The second type of heterogeneity results from the modelling domain chosen for formalising the described system. Usually, this domain is not explicitly described nor formalised. Most of the knowledge related to this domain is hardly encoded by the formal system description. The last decade has made use of ontologies as an explicit formalisation of such modelling domains. Expressing, in formal models, references to ontological concepts contribute to reduce such a heterogeneity. It also allows developers to address specific properties related to interoperable, adaptive, reconfigurable and plastic systems.

This thematic track is devoted to compile the state of the art in heterogeneous formal developments. It will highlight the recent advances in this research field. Particularly welcome are reports, research and position papers, issued either from the academic or industrial worlds,presenting

• original contributions
• work - in - progress
• position papers
• experiments on industrial case studies.

The Special Track will be part of the 5^th ISoLA International Symposium on Leveraging Applications of Formal Methods, Verification and Validation.

Topics of interest include (but are not limited to):

• Multi-modelling and meta-modelling formal techniques
• Definition of unified theories and heterogeneous reasoning
• Validation and verification methods for heterogeneous formal models
• Formal verification of Adaptive, interoperable, reconfigurable ... systems
• Specification, design and architecture languages
• Ontology based formal modelling
• Domain ontologies and explicit model annotation
• Ontology based reasoning for formal verification
• Formal models for ontologies and formal models annotation

Track Organizers

Yamine Ait-Ameur (F), Dominique Mery (F)

Formal Methods for Intelligent Transportation Systems

The term Intelligent Transportation Systems (ITS) refers to information and communication technology (applied to transport infrastructure and vehicles) that improve transport outcomes such as transport safety, transport productivity, travel reliability, informed travel choices, social equity, environmental performance and network operation resilience. Safety-critical ITS include the so called X-by-wire (where 'X' can stand for 'fly', 'brake', 'accelerate, 'steer', etc.) systems used in domains like aerospace, automotive and railways. The importance of ITS is increasing as novel driverless/pilotless applications are emerging. This track addresses the application of formal methods to model and analyze complex systems in the context of ITS. In fact, modeling and analysis activities are very important to optimize system life-cycle in the design, development, verification and operational stages, and they are essential whenever assessment and certification is required by international standards. In this regard, several approaches suggest a specification methodology based on the Unified Modeling Language (UML), together with its extensions/profiles, to generate analyzable formal models. Methodologies integrating the requirements of incremental and modular development are especially challenging. Both qualitative and quantitative evaluations can be performed on formal models, including model-checking and stochastic simulations. Finally, on-line model-checking (e.g. for adaptive route planning) issues are also very important in the context of ITS, when objects exchange information about their states to reach consistency among their decisions.

Track Organizers

Alessandro Fantechi (DSI - Univ. of Florence), Francesco Flammini (Ansaldo STS), Stefania Gnesi (ISTI - CNR - Pisa)