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), Kim Larsen (DK)
-
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)
-
Approaches 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)
-
Linux Driver Verification
Organizers: Dirk Beyer (University of Passau, Germany), Alexander K. Petrenko (ISPRAS, Moscow, Russia)
-
Processes and data integration in the networked healthcare
Organizers: A. Braun v. Reinersdorff (), T. Margaria (), C. Rasche ()
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), Kim Larsen (DK)
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)
Approaches 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)
LearnLib Tutorial: From finite automata to register interface programs
...
Track Organizers
... (..., .)
The ITSy Day 2012
...
Track Organizers
... (..., .)
*/ ?>
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)
Content
-
Sieber, René ;
Eichenberger, Remo
(ETH Zürich): Concepts, processes and techniques of 3d online
atlases
-
Borg, Erik ;
Fichtelmann, Bernd ;
Asche, Hartmut
(DLR Neustrelitz): Process Control based on Data Usability for
Deriving Remote Sensing Value Added Data Products
-
Nitze, Ingmar ;
Schulthess, Urs ;
Asche, Hartmut
(Department of Geography, University College Cork): Comparison of
topical machine learning algorithms (random forest, artificial
neural network, support vector machine) with maximum likelihood for
supervised crop type classification
-
Asche, Hartmut ;
Engemaier, Rita
(FG Geoinformatik, Universität Potsdam): Web-based on-demand
service for the generation of quality maps: concept and processing
pipeline
-
Rogass, Christian
(GFZ Potsdam): Modelling of canopy reflectance using botanical
and physically.based 3D mockups for remote sensing applications
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 5th 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)
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)
The goal of the track on Linux driver verification is to bring together
researchers and practitioners that work in the area of functional, safety,
and security verification of real-life software written in C. The research
in program analysis, SMT solvers, model checking, and other areas of
software verification has made a significant progress in terms of
precision and performance. State-of-the-art verification tools have
become applicable to real-life
software such as device drivers (cf. SV-COMP'12). At the same time, many new
issues appear that were not important in previous settings. The LDV track
provides a forum to discuss specifics of real-world verification of C
programs, new issues that appear on the way, and experiences gained.
The track is devoted to Linux device-driver verification, because the
Linux kernel-space code is different from usual C programs in several
aspects. At the same time, this code base is a very popular target for
many research projects for various reasons.
The track provides an opportunity to share experience and to establish
collaboration between different projects in the domain.
Track Organizers
Dirk Beyer (University of Passau, Germany), Alexander K. Petrenko (ISPRAS, Moscow, Russia)
Track Organizers
A. Braun v. Reinersdorff (), T. Margaria (), C. Rasche ()