Tracks
-
Emerging services and technologies for a
converging Telecommunications / Web world in smart environments
of the Internet of Things
Organizers: Noel Crespi (Institut Telecom, France); Gyu
Myoung Lee (Institut Telecom, France); Thomas Magedanz (Fraunhofer
FOKUS/TU Berlin, Germany)
-
Learning Techniques for Software Verification
and Validation
Organizers: Dimitra Giannakopoulou (CMU/NASA Ames); Corina
Pasareanu (CMU/NASA Ames)
-
Modeling and Formalizing Industrial Software
for Verification, Validation and Certification
Organizers: Alexander K. Petrenko (ISPRAS, Moscow);
Rostislav Yavorskiy (Microsoft Research, Cambridge
UK/Moscow)
-
Formal Methods in Model-Driven Development for
Service-Oriented and Cloud Computing
Organizers: Stefania Gnesi (ISTI-CNR, PISA); Howard Foster
(Department of Computing, City University London); Laura Semini
(Dipartimento di Informatica Università di Pisa)
-
Tools in Scientific Workflow
Composition
Organizers: Joost Kok (Leiden Institute of Advanced Computer
Science Leiden University); Anna-Lena Lamprecht (TU Dortmund);
Mark D. Wilkinson (Heart + Lung Institute at St. Paul's
Hospital, Vancouver, BC, Canada)
-
New challenges in the development of critical
embedded systems - an "aeromotive"
perspective
Organizers: Visar Januzaj (TU Darmstadt); Stefan Kugele (TU
Muenchen); Boris Langer (Diehl Aerospace); Christian Schallhart
(TU Darmstadt); Helmut Veith (TU Wien)
-
Web Science
Organizers: Marco Antonio Casanova (PUC-Rio); Karin Breitman
(PUC-Rio); Amal Seghrouchni (Université Pierre et Marie Curie,
France); Michael Hinchey (Lero - The Irish Software Engineering
Research Centre, Ireland)
-
Leveraging formal methods through
collaboration
Organizers: Pierre-Loïc Garoche (ONERA); Rémi Delmas
(ONERA)
-
Resource and Timing Analysis
Organizers: Kevin Hammond, Univ. of St. Andrews, Scotland;
Jens Knoop, TU Vienna, Austria; Björn Lisper, Mälardalen
University, Sweden; Pascal Montag, Daimler AG, Germany
-
Quantitative Verification in Practice
Organizers: Boudewijn Haverkort (Embedded Systems Institute,
NL); Joost-Pieter Katoen (RWTH Aachen University, D); Kim G.
Larsen (Center for Embedded Software Systems, DK);
-
Worst Case Traversal Time (WCTT)
Organizers: Anne Bouillard (ENS Cachan, F); Marc Boyer
(ONERA, F); Samarjit Chakraborty (Technische Universität
München, D); Jean-Luc Scharbarg (IRIT, F); Steven Martin (LRI,
F); Eric Thierry (ENS Lyon, F); Giovanni Stea (Pisa University,
I);
-
Model Transformation and Analysis for
Industrial Scale Validation
Organizers: He Jifeng, East China Normal University,
Shanghai; Zhiming Liu, UNU-IIST, Macao; Abhik Roychoudhury,
NUS, Singapore
-
Certification of Software-Driven Medical
Devices
Organizers: Alan Wassyng, McMaster University, Canada; Tom
Maibaum, McMaster University, Canada; Mark Lawford, McMaster
University, Canada
-
Formal languages and methods for designing
and verifying complex engineering systems
Organizers: Yamine Ait Ameur (LISI/ENSMA- Poitiers- France;
Frédéric Boniol(IRIT/ENSEEIHT - Toulouse France); Dominique
Mery (LORIA – Nancy Université - France); Virginie Wiels
(ONERA/DTIM- Toulouse France)
-
CONNECT: Status and Plan
Organizers: Valrie Issarny (INRIA, FR)
-
EternalS: Mission and Roadmap
Organizers: Alessandro Moschitti (University of Trento, IT)
-
ISoLA-Panel: Usable Verification
Organizers: Lenore Zuck (University of Illinois at Chicago,
IL USA)
Emerging services and technologies for a
converging Telecommunications / Web world in smart environments
of the Internet of Things
The telecommunications, internet and information technology
worlds are converging. The Internet of Things, which refers a
network of objects and provides smart environments for the
deployment of numerous applications, will have a significant
impact on many fields of future everyday life. In this context
emerging Service Oriented Architectures (SOAs) over the next
generation of fixed and mobile networks are considered to be of
key importance for the rapid and efficient creation, provisioning
and delivery of seamless multimedia information and communication
services. The Web 2.0/3.0 world will accelerate user-centric
services through service compositions/mash-ups and semantic
web/ontology in open environments. In addition, various computing
technologies such as cloud computing will enable the provision of
services in more cost-effective ways. In this mini-track we want
to provide a snapshot of the current issues and possible
solutions for emerging services in a converging
Telecommunications / Web-based smart environments
Track Organizers
Noel Crespi, Institut Telecom, France
Gyu Myoung Lee, Institut Telecom, France
Thomas Magedanz, Fraunhofer FOKUS/TU Berlin, Germany
Content
-
Invited talk: "Approaches to Integrative Telco
Service Architectures for the WebX.0"
Ernst-Joachim Steffens, Deutsch Telekom, Germany
- Towards More Adaptive Voice Applications
Jörg Ott
-
Invited talk: "The role of testbeds in the
implementation of the Future Internet PPP"
Anastasius Gavras, EURESCOM
- Telco Service Delivery Platforms in the last decade - a
R&D perspective
Sandford Bessler
- Ontology-Driven Pervasive Service Composition for Everyday
Life
Jiehan Zhou, Ekaterina Gilman, Jukka Riekki, Mika
Rautiainen, and Mika Ylianttila
- Navigating the Web of Things: visualizing and interacting
with Web-enabled objects
Mathieu Boussard and Pierrick Thébault
- Shaping Future Service Environments with the Cloud and
Internet of Things: Networking Challenges and Service Evolution
Gyu Myoung Lee and Noel Crespi
- Relay Placement Problem in Smart Grid Deployment
Wei-Lun Wang and Quincy Wu
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. Such models can serve as formal
documentation of the software and they can be further verified
using automated tools or used for model-based test case
generation. 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, various
machine-learning techniques have been used in fine-tuning
heuristics used in constraint solving, in coming up with new
abstraction techniques in the context of bounded model checking
or shape analysis, in inferring invariants of parameterized
systems, 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 2010 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 Components
- Automated Compositional Verification
- Requirements Elicitation and Analysis
- Abstraction Refinement and Shape Analysis
- Symbolic and Parameterized Verification
- Decision Procedures and Constraint Solving
- Black-box and White-box Testing
- Improving practical applications in avionics,
telecommunications, etc.
Track Organizers
Dimitra Giannakopoulou, CMU/NASA Ames
Corina Pasareanu, CMU/NASA Ames
Content
- Overview of the field, and of the goals of the track
Dimitra Giannakopoulou and Corina Pasareanu
-
Invited talk: "Learning NFAs"
Martin Leucker
- Comparing Learning Algorithms in Automated Assume-Guarantee
Reasoning
Yu-Fang Chen, Edmund M. Clarke, Azadeh Farzan, Fei He,
Ming-Hsien Tsai, Yih-Kuen Tsay, Bow-Yaw Wang, and Lei Zhu
- Inferring Compact Models of Communication Protocol Entities
Therese Berg, Bengt Jonsson, and Siavash Soleimanifard
- Inference and Abstraction of the Biometric Passport
Fides Aarts, Julien Schmaltz, and Frits Vaandrager
-
Invited talk: "From Zulu to RERS"
Falk Hower, Maik Merten, and Bernhard Steffen
Modeling and Formalizing Industrial
Software for Verification, Validation and Certification
Several aspects of software quality including reliability,
interoperability, portability need methodological and tool
support. Key issue of such methodologies is a formalization of
requirements and other functional and nonfunctional properties.
Formalization is a promising way to automated verification and
certification of industrial software and computer intensive
systems as a whole.
This Special Track aims at bringing together researchers working
on the integration of lightweight formal and model-based
techniques with practitioners and experts from industry. The
Special Track will be part of the 2010 ISoLA International
Symposium on Leveraging Applications of Formal Methods,
Verification, and Validation.
Topics of interests:
- Formalization of API, Programming Language, Telecommunication
Protocol Standards
- Portability and Interoperability Testing
- Model Based Testing
- Modeling and Verification of Domain-specific Business and
Safety Rules
- Verification and Validation of Avionic and Automotive Systems
- Specification and Verification of Distributed and Component
Software
- Verification of Hardware Design
- Information Infrastructure for Software Standards Compliance
Certification
Track Organizers
Alexander K. Petrenko, ISPRAS, Moscow
Rostislav Yavorskiy, Microsoft Research, Cambridge
UK/Moscow
Content
- Improving Portability of Linux Applications by Early
Detection of Interoperability Issues
Denis Silakov and Andrey Smachev
- Specification Based Conformance Testing for Email Protocols
Nikolay Pakulin and Anastasia Tugaenko
- Covering arrays generation methods survey
Victor Kuliamin and Alexander Petukhov
Formal Methods in Model-Driven
Development for Service-Oriented and Cloud Computing
In Model Driven Development, systems are built by transforming
models from higher levels of abstraction to the point where we
reach a model which is executable. Formal methods can play many
roles in MDD. Along the main development spine they can define
formal modelling languages, metamodels and transformations, and
supply tools to transform a model in a more concrete one. At each
develompment step, formal methods can be used to evaluate the
correctness and the quality of the intermediate models. In this
role, they apply directly to the models in the spine or to barbs
that introduce specialized models. These tools permit specific,
sometimes very sophisticated, analysis of part of the software.
This special track is devoted to the definition and application
of formal methods to the Model Driven Development of systems
based on the Service Oriented Architecture and on Cloud
Computing, with particular interest for:
- metamodelling and transformation frameworks
- quantitative and qualitative evaluation tools
- barbed MDD
- domain specific modelling
- model based testing
- experience reports and case studies on very large scale
industrial
- current and future challenges for FM and MDD
Track Organizers
Stefania Gnesi, ISTI-CNR, Pisa
Howard Foster, Department of Computing, City University
London
Laura Semini, Dipartimento di Informatica, Università di
Pisa
Content
- Adaptive Composition of Conversational Services through Graph
Planning Encoding
Pascal Poizat and Yuhong Yan
- Performance Prediction of Service-Oriented Systems with
Layered Queueing Networks
Mirco Tribastone, Philip Mayer, and Martin Wirsing
- Error Handling: from Theory to Practice
Ivan Lanese and Fabrizio Montesi
- Modeling and Reasoning about Service Behaviors and their
Compositions
Aida Causevic, Cristina Seceleanu, and Paul Pettersson
- Design and Verification of Systems with Exogenous
Coordination using Vereofy
Christel Baier, Tobias Blechmann, Joachim Klein, Sascha
Klüppelholz, and Wolfgang Leister
- A Case Study in Model-based Adaptation of Web Services
Javier Camara, Jose Antonio Martin, Gwen Salaün, Carlos
Canal, and Ernesto Pimentel
Tools in Scientific Workflow Composition
This special track aims at bringing together researchers and
practitioners from bioinformatics and other application areas who
are interested in the various topics connected to the composition
of scientific workflows.
Topics of interest for this track include (but are not limited
to):
- tools and frameworks for workflow composition
- social networks for workflows
- service discovery methods
- ontologies for the description of services and data
- service and data type semantics
- semantically aware workflow development
- automatic workflow composition
- case studies, examples and experiences
Track Organizers
Joost Kok, Leiden Institute of Advanced Computer Science
Leiden University
Anna-Lena Lamprecht, TU Dortmund
Mark D. Wilkinson, Heart + Lung Institute at St.
Paul's Hospital, Vancouver, BC, Canada
Content
- Tools in Scientific Workflow Composition
Joost N. Kok, Anna-Lena Lamprecht, and Mark D. Wilkinson
- Workflows for Metabolic Flux Analysis: Data Integration and
Human Interaction
Tolga Dalman, Peter Droste, Michael Weitzel, Wolfgang
Wiechert, and Katharina Nöh
- Intelligent Document Routing in SQL: a Case Study
Carlos Soares and Miguel Calejo
- Combining Subgroup Discovery and Permutation Testing to
Reduce Reduncancy
Jeroen S. de Bruin and Joost N. Kok
- Semantically-guided Workflow Construction in Taverna – The
SADI and BioMoby Plugins
David Withers, Edward Kawas, Luke McCarthy, Benjamin
Vandervalk, and Mark Wilkinson
- Workflow Construction for Service-Oriented Knowledge
Discovery
Vid Podpecan, Monika Zakova, and Nada Lavrac
- Workflow composition and enactment using jORCA
Johan Karlsson, Victoria Martín-Requena, Javier Ríos, and
Oswaldo Trelles
- A Linked Data Approach to Sharing Workflows and Workflow
Results
Marco Roos, Sean Bechhofer, Jun Zhao, Paolo Missier, David
R. Newman, David De Roure, and M. Scott Marshall
New challenges in the development of
critical embedded systems - an "aeromotive" perspective
During the last decades, embedded systems have become
increasingly important in highly safety-critical areas such as
power plants, medical equipment, cars, and airplanes. The
automotive and avionics domains are prominent examples of
classical engineering disciplines where conflicts between costs,
short product cycles and legal requirements concerning
dependability, robustness, security, carbon footprint and spatial
demands have become a pressing problem. This setting necessitates
a disciplined, rigorous systems engineering which is able to find
good trade-offs between complex and conflicting requirements.
This special track will facilitate the exchange between the
industrial and academic communities involved in the development
of automotive and avionics systems. The special track will be
part of the 2010 ISoLA International Symposium on Leveraging
Applications of Formal Methods,Verification, and Validation.
Topics of interest include (but are not limited to)
- Specification, design, and architectural languages
- Requirements specification and management
- Evaluation of architectural alternatives
- System configuration and optimization
- Model-based engineering
- Integration/Application of AUTOSAR and IMA in system
development
- Software/Hardware co-design and integration
- Formal methods for critical systems
- Certification
- Case studies in the avionics and automotive industries
Track Organizers
Visar Januzaj (TU Darmstadt)
Stefan Kugele (TU Muenchen)
Boris Langer (Diehl Aerospace)
Christian Schallhart (TU Darmstadt)
Helmut Veith (TU Wien)
Content
- New Challenges in the Development of Critical Embedded
Systems - an "aeromotive" Perspective
Visar Januzaj, Stefan Kugele, Boris Langer, Christian
Schallhart, and Helmut Veith
- Certification of Embedded Software – Impact of ISO DIS 26262
in the Automotive Domain
Bernhard Schätz
- Enforcing Applicability of Real-time Scheduling Theory
Feasibility Tests with the use of Design-Patterns
Alain Plantec, Frank Singhoff, Pierre Dissaux, and Jérôme
Legrand
- Seamless Model-driven Development put into Practice
Wolfgang Haberl, Markus Herrmannsdoerfer, Stefan Kugele,
Michael Tautschnig, and Martin Wechs
- Timely Time Estimates
Andreas Holzer, Visar Januzaj, Stefan Kugele, and Michael
Tautschnig
- Compiler-Support for Robust Multi-Core Computing
Raimund Kirner, Stephan Herhut, and Sven-Bodo Scholz
Web Science
The World Wide Web (the Web for short) has had a tremendous
impact on scientific research, technological development and
human experience and society. The ways we communicate,
collaborate and learn are being radically changed by it. As an
entity, however, it remains surprisingly unstudied
This motivated the appearance, in 2006, of a new research domain
– the so-called Web Science [Berners-Lee et al. 2006, Hendler et
al. 2008]. In this new domain, the Web is the primary object of
study and ceases to be viewed as a mere technology, based on
computers, that helps people communicate and interact on a global
basis. As such, it involves not only research on computing and
technological aspects, but also on social and economic issues.
More precisely, it is the science that investigates all issues
around decentralized information systems, covering people,
software and hardware, and their multiple, complex interactions.
Indeed, the significance of the Web depends not only on its
computational properties, but also on the context of its use.
Understanding the multiple relationships between the Web and
society at a number of scales, from computer science and
mathematics to emergent social behavior, has become an essential
research agenda to ensure the Web’s growth and contribution to
society.
The aim of the track is to bring together researchers interested
in exploring the various facets of this exciting area. We invite
contributions in, but not limited to the following areas:
- Interaction Design
- Social Networks
- Web and the Individual
- Web and politics
- Multi agent systems
- Model-driven design and implementation of web applications
- Design and implementation of Autonomic workflows
- Security and Privacy
- Web based collaborative environments
- Virtual web environments
- Semantic web
- Integration of Web information sources
- Knowledge discovery on the web
- Future internet architectures
- Ubiquitous and location aware web
- Algorithms and complexity for the Web graph
- Modeling the Web
- Trust and Reputation
- Culture on-line
- Cloud computing
- eScience
Track Organizers
Marco Antonio Casanova (chair)
Karin Breitman - PUC-Rio
Amal Seghrouchni - Université Pierre et Marie Curie,
France
Michael Hinchey - Lero - The Irish Software Engineering
Research Centre, Ireland
Content
- Towards a Research Agenda for Enterprise Crowdsourcing
Maja Vukovic and Claudio Bartolini
- Analyzing Collaboration in Software Development Processes
through Social Networks
Andréa Magalhães Magdaleno, Cláudia Maria Lima Werner, and
Renata Mendes de Araujo
- A Web-based Framework for Collaborative Innovation
Donald Cowan, Paulo Alencar, Fred McGarry, Carlos Lucena,
and Ingrid Nunes
- A Distributed Dynamics for Web Graph Decontamination
Vanessa C. F. Gonçalves, Priscila M. V. Lima, Nelson
Maculan, and Felipe M. G. França
- Increasing Users' Trust on Personal Assistance Software
using a Domain-neutral High-level User Model
Ingrid Nunes, Simone D.J. Barbosa, and Carlos J.P. de
Lucena
- Understanding IT Organizations
Claudio Bartolini, Karin Breitman, Simone Diniz Junqueira
Barbosa, Mathias Salle, Rita Berardi, Glaucia Melissa Campos,
and Erik Eidt
- On the 2-Categorical View of Proofs
Cecilia Englander and Edward Hermann Haeusler
Leveraging formal methods through
collaboration.
Formal design methods for producing correct-by-construction
software,or verification methods such as model checking, abstract
interpretation, deductive methods, theorem proving, etc. have
been around for 30 years and have matured up to the point where
they can be used in the industry, and start being considered as
viable options to traditional unsound and/or incomplete design
and verification techniques by certification authorities.
Nevertheless, each technique, as mature it can be, comes with
limitations in scope and/or performance. For instance some
techniques are sound but incomplete in the general case, some
others are limited to handling linear arithmetic theories, some
others are dedicated to predefined property templates, some
require manual intervention.
The key ingredient of this track is the presentation of
innovative work on leveraging formal methods for design and
verification through cooperative use of diverse and complementary
methods and techniques.
Contributions could address, but are not limited to, cooperation
of the following methods:
- sound by construction design,
- model checking,
- abstract interpretation,
- model based test case generation,
- constraint satisfaction techniques,
- deductive methods,
- automated abstraction/refinement,
- traditional verification methods,
- etc.
Track Organizers
Pierre-Loïc Garoche (ONERA)
Rémi Delmas (ONERA)
Content
- Thematic Track: Formal Languages and Methods for Designing
and Verifying Complex Embedded Systems
Yamine Ait Ameur, Frédéric Boniol, Dominique Mery, and
Virginie Wiels
- Analyzing the Security in the GSM Radio Network using Attack
Jungles
Parosh Aziz Abdulla, Jonathan Cederberg, and Lisa Kaati
- Formal Modeling and Verification of Sensor Network Encryption
Protocol in the OTS/CafeOBJ Method
Iakovos Ouranos, Petros Stefaneas, and Kazuhiro Ogata
- Model-Driven Design-Space Exploration for Embedded Systems:
The Octopus Toolset
Twan Basten, Emiel van Benthum, Marc Geilen, Martijn
Hendriks, Fred Houben, Georgeta Igna, Frans Reckers, Sebastian
de Smet, Lou Somers, Egbert Teeselink, Nikola Trcka, Frits
Vaandrager, Jacques Verriet, Marc Voorhoeve, and Yang Yang
- Contract-based Slicing
Daniela da Cruz, Pedro Rangel Henriques, and Jorge Sousa
Pinto
Resource and Timing Analysis
Subtrack A: "Scientific Foundations of Resource and Timing
Analysis: Advances and Challenges"
Subtrack B: "Industrial Applications of Resource and Timing
Analysis: Leaving the Ivory Tower"
Embedded systems increasingly permeate the technical
infrastructure we rely on in-the-large as a society, and they
control the technical equipment we rely on in-the-small as
individuals. Many of these systems are safety- and
resource-critical. They have to obey strict specifications for
the consumption of resources such as time, memory, power, and
others in order to be useful. Verifying that these specifications
are fulfilled is very important. A variety of methods and tools
for resource and timing analysis have successfully been launched
by industry, and are being increasingly used in practice: a
challenge is to further increase the precision, power, and
usability of these tools. However, also the foundational aspects
offer a wide range of scientifically exciting research issues and
challenges.
The goal of this special track on "Resource and Timing
Analysis", which splits in the two subtracks on
"Scientific Foundations" and "Industrial
Applications", is to bring together people from academia and
from tool vendors and users in industry who are interested in all
aspects of resource and timing analysis of embedded systems.
Topics of interest include (but are not limited to):
-
foundations and applications of resource analysis for
embedded systems, especially methods and tools for
- memory and power consumption, and
- complexity control.
- Case studies, and academic and industrial experience of
resource analysis.
-
foundations and applications of timing analysis for real-time
embedded systems, especially methods and tools for
- worst-case execution time (WCET) analysis,
- flow analysis for WCET, loop and recursion bounds,
feasible paths.
- Case studies, and academic and industrial experience of
timing analysis.
The special track will foster the exchange between the industrial
and academic communities interested and involved in resource and
timing analysis of embedded systems. The track will be part of
the 2010 ISoLA International Symposium on Leveraging Applications
of Formal Methods, Verification, and Validation.
Track Organizers
Kevin Hammond, Univ. of St. Andrews, Scotland
Jens Knoop, TU Vienna, Austria
Björn Lisper, Mälardalen University, Sweden
Pascal Montag, Daimler AG, Germany
Content
- A Scalable Approach for the Description of Dependencies in
Hard Real-Time Systems
Steffen Kollmann, Victor Pollex, Kilian Kempf, and Frank
Slomka
- Verification of Printer Datapaths using Timed Automata
Georgeta Igna and Frits Vaandrager
- Resource analysis of Automotive/Infotainment systems based on
domain-specific models – a real-world example
Dr. Klaus Birken, Daniel Hünig, Thomas Rustemeyer, and Ralph
Wittmann
- Source-Level Support for Timing Analysis
Gergö Barany and Adrian Prantl
- Practical Experiences of Applying Source-Level WCET Flow
Analysis on Industrial Code
Björn Lisper, Andreas Ermedahl, Dietmar Schreiner, Jens
Knoop, and Peter Gliwa
- Worst-Case Analysis of Heap Allocations
Wolfgang Puffitsch, Benedikt Huber, and Martin Schoeberl
- Partial Flow Analysis with oRange
Marianne de Michiel, Armelle Bonenfant, Clément Ballabriga,
and Hugues Cassé
- Towards an evaluation infrastructure for automotive multicore
real-time operating systems
Jörn Schneider and Christian Eltges
- Context-Sensitivity in IPET for Measurement-Based Timing
Analysis
Michael Zolda, Sven Bünte, and Raimund Kirner
- On the Role of Non-Functional Properties in Compiler
Verification
Jens Knoop and Wolf Zimmermann
Quantitative Verification in Practice
Model checking has been widely accepted by industry for verifying
correctness of hardware and software systems. Temporal logics as
PSL have been accepted as IEEE standard, significant shortcomings
have been established in standardised protocols, and software of
forthcoming NASA missions have been thoroughly checked by tools
such as SPIN. Most systems ---embedded systems in particular---
are subject to a multitude of quantitative constraints. These
constraints involve
- system's resources (computation resources, power
consumption, memory usage, communication bandwidth, etc.),
- assumptions about the environment in which it operates (task
arrival rates, signal fluctuations),
- requirements on the services the system has to provide
(timing constraints, performance), and
- requirements on the continuity with which these services are
delivered (availability, dependability, fault tolerance, etc.).
To meet these challenges quantitative extensions of model
checking have emerged. These include timed automata verification,
checking models that exhibit random phenomena (such as
Markov-like models), and hybrid systems. Powerful tools such as
Uppaal, PRISM, MRMC, PASS and Phaver support this.
The main aim of this track is to show the practical usage of
these techniques. What kind of practically relevant questions can
be answered by these techniques? How is the practical usage of
the tools?, What are their limitations? and so forth.
Track Organizers
Boudewijn Haverkort (Embedded Systems Institute, NL)
Joost-Pieter Katoen (RWTH Aachen University, D)
Kim G. Larsen (Center for Embedded Software Systems, DK)
Content
- Quantitative Verification in Practice
Boudewijn R. Haverkort, Joost-Pieter Katoen, and Kim G.
Larsen
- Ten Years of Performance Evaluation for Concurrent Systems
using CADP
Nicolas Coste, Hubert Garavel, Holger Hermanns, Frédéric
Lang, Radu Mateescu, and Wendelin Serwe
- Towards Dynamic Adaptation of Probabilistic Systems
S. Andova, L.P.J. Groenewegen, and E.P. de Vink
- UPPAAL in Practice: Quantitative Verification of a RapidIO
Network
Jiansheng Xing, Bart D. Theelen, Rom Langerak, Jaco van de
Pol, Jan Tretmans, and J.P.M. Voeten
- Schedulability Analysis Using Uppaal: Herschel-Planck Case
Study
Marius Mikucionis, Kim Guldstrand Larsen, Jacob Illum
Rasmussen, Brian Nielsen, Arne Skou, Steen Ulrik Palm, Jan
Storbank Pedersen, and Poul Hougaard
- Model-Checking Temporal Properties of Real-Time HTL Programs
André Carvalho, Joel Carvalho, Jorge Sousa Pinto, and Simão
Melo de Sousa
Worst Case Traversal Time (WCTT)
Real time systems are more and more communication systems where
functions are implemented by several real-time tasks on different
physical systems (sensors, calculators, actuators). To ensure
global correctness, one have to ensure correctness of each task,
schedulability of tasks on each system, but also to bound the
communication time, ie the worst case (network) traversal time
(WCTT).
Moreover, systems are bigger and bigger, connecting dozens to
hundreds of systems, managing thousands of flows, each one
interacting with others.
This special track is devoted to formal methods on worst case
traversal time in networks, with a special interest on scalable
methods, handling multi-hop networks.
Track Organizers
Anne Bouillard (ENS Cachan, France)
Marc Boyer (ONERA, France)
Samarjit Chakraborty (Technische Universität München,
Germany)
Jean-Luc Scharbarg (IRIT, France)
Steven Martin (LRI, France)
Eric Thierry (ENS Lyon, France)
Giovanni Stea (Pisa University, Italy)
Content
- An Interface Algebra for Estimating Worst-Case Traversal
Times in Component Networks
Nikolay Stoimenov, Samarjit Chakraborty, and Lothar
Thiele
- Towards resource-optimal routing plans for real-time traffic
Alessandro Lori, Giovanni Stea, Gigliola Vaglini
- Partially synchronizing periodic flows with offsets improves
worst-case end-to-end delay analysis of switched Ethernet
Xiaoting Li, Jean-Luc Scharbarg, Christian Fraboul
- Analyzing end-to-end Functional Delays on an IMA Platform
Michael Lauer, Jérôme Ermont, Claire Pagetti, Frédéric
Boniol
- The PEGASE project: precise and scalable temporal analysis
for aerospace communication systems with Network Calculus
Marc Boyer, Nicolas Navet, Xavier Olive, and Eric
Thierry
- NC-maude: a rewriting tool to play with network calculus
Marc Boyer
- DEBORAH: A Tool for Worst-case Analysis of FIFO Tandems
Luca Bisti, Luciano Lenzini, Enzo Mingozzi, and Giovanni
Stea
- A Self-Adversarial Approach to Delay Analysis under Arbitrary
Scheduling
Jens B. Schmitt, Hao Wang, and Ivan Martinovic
- Flow Conrtrol with (Min,+) Algebra
Euriell Le Corronc, Bertrand Cottenceau, and Laurent
Hardouin
Model Transformation and Analysis for
Industrial Scale Validation
Modern system software applications are becoming increasingly
complex. As in all successful engineering disciplines, building
models is the only effective way of mastering the complexity and
to develop tool support in their design, validation and
verification. In component-based approach, each phase in the
software development is based on building models. Models in a
later stage are obtained through transformations from models
built earlier. Models must be validated, analyzed and verified.
Tools support in model construction, transformation, validation
and verification is crucial for the predictability and
reliability of software development projects. This Special Track
aims at bringing together researchers and practitioners to
exchange theoretical ideas, techniques and practical experiments
in component-based software development. The topics include, but
not restricted to, the following three strands:
-
Model-based techniques for designs (including model
transformations), analysis, verification and refactoring of
- component, object and web-service software
- embedded systems
- Cyber-Physical Systems (CPS)
-
Tools for model transformation, integration, analysis and
verification
-
Industrial aplications, such as enterprise systems, health
care systems, railway control systems
Track Organizers
He Jifeng (East China Normal University, Shanghai)
Zhiming Liu (UNU-IIST, Macao)
Abhik Roychoudhury (NUS, Singapore)
Content
- WOMM: A Weak Operational Memory Model
Arnab De, Abhik Roychoudhury, and Deepak D’Souza
- A Memory Model for Static Analysis of C Programs
Zhongxing Xu, Ted Kremenek, and Jian Zhang
- Analysing Message Sequence Graph Specifications
Joy Chakraborty, Deepak D’Souza, and K Narayan Kumar
- Optimize Context-Sensitive Andersen-style Points-to Analysis
by Method Summarization and Cycle-Elimination
Li Qian, Zhao Jianhua, and Li Xuandong
- A Formal Analysis of the Web Services Atomic Transaction
Protocol with UPPAAL
Anders P. Ravn, Jiri Srba, and Saleem Vighio
- SPARDL: A Requirement Modeling Language for Periodic Control
System
Zheng Wang, Jianwen Li, Yongxin Zhao, Yanxia Qi, Geguang Pu,
Jifeng He, and Bin Gu
- AutoPA: Automatic Prototyping from Requirements
Xiaoshan Li, Zhiming Liu, Martin Schäf, and Ling Yin
- Systematic Model-Based Safety Assessment via Probabilistic
Model Checking
Adriano Gomes, Alexandre Mota, Augusto Sampaio, Felipe
Ferri, and Julio Buzzi
Certification of Software-Driven
Medical Devices
Medical devices that are dependant on software for their
operation have proven to be a challenge for regulators and
manufacturers. This track will focus on approaches that the
formal methods community could recommend to regulators that will
improve the predictability of the certification process for both
the regulator and the manufacturer, as well as the effectiveness
of the certification itself.
Topics of interest include (but are not limited to):
- The PACEMAKER Challenge - specifically related to
certification
- Safety-case approaches for medical devices - pros and cons
- Practical approaches and notations for formal requirements
- Forensic software tools and their role in certification
- Prescriptive versus non-prescriptive certification
- Qualification of tools used to develop medical-device
software
- Should testing be supplemented by mathematical
analysis/verification?
- How much of the development process should be of concern to
the certifier?
- How do we certify devices built through model-driven
development?
- Can we certify devices without access to all the source code?
Track Organizers
Alan Wassyng (McMaster University, Canada)
Tom Maibaum (McMaster University, Canada)
Mark Lawford (McMaster University, Canada)
Content
- Certification of Software-Driven Medical Devices
Mark Lawford, Tom Maibaum, and Alan Wassyng
- Arguing for Software Quality in an IEC 62304 Compliant
Development Process
Michaela Huhn and Axel Zechner
- Design Choices for High-Confidence Distributed Real-time
Software
Sebastian Fischmeister and Akramul Azim
- Trustable Formal Specification for Software Certification
Dominique Méry and Neeraj Kumar Singh
- Assurance Cases in Model-Driven Development of the Pacemaker
Software
Eunkyoung Jee, Insup Lee, and Oleg Sokolsky
Formal languages and methods for
designing and verifying complex engineering systems
Due to safety constraints, complex systems like avionics,
aerospace, transport systems, telecom, etc. often have to go
through certification. This requires testing, and a design
process based on a set of tight rules. However, due to the
increasing complexity of described systems, there is clearly no
guarantee that such tight rules and rigorous testing will lead to
error free systems. An alternative approach for helping system
designers is formal methods, i.e. fundamental languages,
techniques and tools for design, analysis, validation or
transformation of systems in a provably correct way.
Indeed, formal techniques, in particular formal specification
languages and associated proof tools, could be an advantageous
alternative or at least a good complement which would facilitate
a significant reduction in test phases. Several formal languages
methods, tools and techniques have been applied for the
development of such systems in different parts of the world and
they have been put into practice during the development of
actual, specific programmes (aircraft, space vehicle…).
This thematic track is devoted to compile the state-of-the-art in
formal methods applied to the development of complex systems. It
will highlight on the recent advances in the use of these
methods. 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 2010 ISoLA International
Symposium on Leveraging Applications of Formal Methods,
Verification and Validation.
Topics of interest include (but are not limited to):
- specification, design and architecture languages
- validation and verification methods for critical embedded
systems, such as model checking, proof based techniques…
- functional requirements engineering
- methods for human-machine interface verification
- techniques and tools for modelling systems of systems
- model heterogeneity reduction
- case studies and project results with applications in the
context of transport, telecom, system engineering, etc.
Track Organizers
Yamine Ait Ameur (LISI/ENSMA- Poitiers- France)
Frédéric Boniol (IRIT/ENSEEIHT - Toulouse France)
Dominique Mery (LORIA – Nancy Université - France)
Virginie wiels (ONERA/DTIM- Toulouse France)
Content
- Formal Languages and Methods for Designing and Verifying
Complex Embedded Systems
Yamine Ait Ameur, Frédéric Boniol, Dominique Mery, and
Virginie Wiels
- Analyzing the Security in the GSM Radio Network using Attack
Jungles
Parosh Aziz Abdulla, Jonathan Cederberg, and Lisa Kaati
- Formal Modeling and Verification of Sensor Network Encryption
Protocol in the OTS/CafeOBJ Method
Iakovos Ouranos, Petros Stefaneas, and Kazuhiro Ogata
- Model-Driven Design-Space Exploration for Embedded Systems:
The Octopus Toolset
Twan Basten, Emiel van Benthum, Marc Geilen, Martijn
Hendriks, Fred Houben, Georgeta Igna, Frans Reckers, Sebastian
de Smet, Lou Somers, Egbert Teeselink, Nikola Trcka, Frits
Vaandrager, Jacques Verriet, Marc Voorhoeve, and Yang Yang
- Contract-based Slicing
Daniela da Cruz, Pedro Rangel Henriques and Jorge Sousa
Pinto
CONNECT: Status and Plan
Please, find more information on the website of the project.
Track Organizers
Valrie Issarny (INRIA, FR)
Content
- Towards an Architecture for Runtime Interoperability
Amel Bennaceur, Gordon Blair, Franck Chauvel, Huang Gang,
Nikolaos Georgantas, Paul Grace, Falk Howar, Paola Inverardi,
Valrie Issarny, Massimo Paolucci, Animesh Pathak, Romina
Spalazzese, Bernhard Steffen, and Bertrand Souville
- On Handling Data in Automata Learning - Considerations from
the CONNECT Perspective
Falk Howar, Bengt Jonsson, Maik Merten, Bernhard Steffen,
Sofia Cassel
- A Theory of Mediators for Eternal Connectors
Paola Inverardi, Valérie Issarny, and Romina Spalazzese
- On-the-fly Interoperability through Automated Mediator
Synthesis and Monitoring
Antonia Bertolino, Paola Inverardi, Valérie Issarny,
Antonino Sabetta, and Romina Spalazzese
- Dependability Analysis and Verification for Connected Systems
Felicita Di Giandomenico, Marta Kwiatkowska, Marco
Martinucci, Paolo Masci, and Hongyang Qu
- Towards a Connector Algebra
Marco Autili, Chris Chilton, Paola Inverardi1, Marta
Kwiatkowska, and Massimo Tivoli
EternalS: Mission and Roadmap
Please, find more information on the website of the project.
Track Organizers
Alessandro Moschitti (University of Trento, IT)
Content
- Introduction to the EternalS Track: Trustworthy Eternal
Systems via Evolving Software, Data and Knowledge
Alessandro Moschitti
- HATS: Highly Adaptable and Trustworthy Software using Formal
Methods
Reiner Hähnle
- SecureChange: Security Engineering for Lifelong Evolvable
Systems
Riccardo Scandariato and Fabio Massacci
- 3DLife: Bringing the Media Internet to Life
Ebroul Izquierdo, Tomas Piatrik and Qianni Zhang
- LivingKnowledge: Kernel Methods for Relational Learning and
Semantic Modeling
Alessandro Moschitti
- Task Forces in the EternalS Coordination Action
Reiner Hähnle
- Modeling and Analyzing Diversity - Description of EternalS
Task Force 1
Ina Schaefle
- Modeling and Managing System Evolution Description of
EternalS Task Force 2
Michael Hafner
- Self-adaptation and Evolution by Learning - Description of
EternalS Task Force 3
Richard Johansson
- Overview of Roadmapping by EternalS
Jim Clarke and Keith Howker
ISoLA panel: Usable Verification
In spite of rapid progress in the area of software design,
analysis, and verification (“formal methods”), the impact of the
newly developed methodologies on industry is, at best, scant.
This can be contrasted with hardware verification, where novel
formal methodologies are rapidly incorporated in the design of
“real” systems. Applying formal methods to software is obviously
harder than applying them to hardware, and currently requires
expertise held by few, which renders the new methodologies
useless. We believe that making formal methods usable to the
developers of the systems for which they are intended, requires
significant effort from the formal methods research community.
Approaches to software verification studied in conferences
focusing on formal methods, such as CAV, TACAS, and VMCAI,
usually offer methods that are almost fully automatic, are able
to verify only the simplest properties, and are applicable only
to a few examples. The goal of the panel is to discuss approaches
to "Usable Verification" that would allow formal
techniques to be applied to software verification in industrial
setting. The panel will bring together academics who developed
formal methods, and industry representatives who have worked on
their application to industrial domains. We'd appreciate if
you can join the panel.
Track Organizers
Lenore Zuck (University of Illinois at Chicago, IL USA)