»Home | »Call for Papers | »Committees | »Tracks | »Co-located Events | »Program | »Paper Submission | »General Information | »Registration | »Accommodation | »ISoLA |

ISoLA-Week Schedule

16-17  Soft Skills Course
17  RERS Challenge
17-21  ITSy Panel Meetings
18-20  ISoLA Symposium
21  EternalS Project Meeting

ISoLA 2010 Deadlines:

Early Registration:
September 19th, 2010

Co-located Events at the ISoLA Week:

Tracks

Symposium Chair

Tiziana MARGARIA
(Univ. Potsdam, D)
margaria[at]cs.uni-potsdam.de

Program Chair

Bernhard STEFFEN
(TU Dortmund, D)
steffen[at]cs.uni-dortmund.de

Tracks

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

  1. Invited talk: "Approaches to Integrative Telco Service Architectures for the WebX.0"
    Ernst-Joachim Steffens, Deutsch Telekom, Germany
  2. Towards More Adaptive Voice Applications
    Jörg Ott
  3. Invited talk: "The role of testbeds in the implementation of the Future Internet PPP"
    Anastasius Gavras, EURESCOM
  4. Telco Service Delivery Platforms in the last decade - a R&D perspective
    Sandford Bessler
  5. Ontology-Driven Pervasive Service Composition for Everyday Life
    Jiehan Zhou, Ekaterina Gilman, Jukka Riekki, Mika Rautiainen, and Mika Ylianttila
  6. Navigating the Web of Things: visualizing and interacting with Web-enabled objects
    Mathieu Boussard and Pierrick Thébault
  7. Shaping Future Service Environments with the Cloud and Internet of Things: Networking Challenges and Service Evolution
    Gyu Myoung Lee and Noel Crespi
  8. 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:

Track Organizers

Dimitra Giannakopoulou, CMU/NASA Ames
Corina Pasareanu, CMU/NASA Ames

Content

  1. Overview of the field, and of the goals of the track
    Dimitra Giannakopoulou and Corina Pasareanu
  2. Invited talk: "Learning NFAs"
    Martin Leucker
  3. 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
  4. Inferring Compact Models of Communication Protocol Entities
    Therese Berg, Bengt Jonsson, and Siavash Soleimanifard
  5. Inference and Abstraction of the Biometric Passport
    Fides Aarts, Julien Schmaltz, and Frits Vaandrager
  6. 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:

Track Organizers

Alexander K. Petrenko, ISPRAS, Moscow
Rostislav Yavorskiy, Microsoft Research, Cambridge UK/Moscow

Content

  1. Improving Portability of Linux Applications by Early Detection of Interoperability Issues
    Denis Silakov and Andrey Smachev
  2. Specification Based Conformance Testing for Email Protocols
    Nikolay Pakulin and Anastasia Tugaenko
  3. 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:

Track Organizers

Stefania Gnesi, ISTI-CNR, Pisa
Howard Foster, Department of Computing, City University London
Laura Semini, Dipartimento di Informatica, Università di Pisa

Content

  1. Adaptive Composition of Conversational Services through Graph Planning Encoding
    Pascal Poizat and Yuhong Yan
  2. Performance Prediction of Service-Oriented Systems with Layered Queueing Networks
    Mirco Tribastone, Philip Mayer, and Martin Wirsing
  3. Error Handling: from Theory to Practice
    Ivan Lanese and Fabrizio Montesi
  4. Modeling and Reasoning about Service Behaviors and their Compositions
    Aida Causevic, Cristina Seceleanu, and Paul Pettersson
  5. Design and Verification of Systems with Exogenous Coordination using Vereofy
    Christel Baier, Tobias Blechmann, Joachim Klein, Sascha Klüppelholz, and Wolfgang Leister
  6. 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):

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

  1. Tools in Scientific Workflow Composition
    Joost N. Kok, Anna-Lena Lamprecht, and Mark D. Wilkinson
  2. Workflows for Metabolic Flux Analysis: Data Integration and Human Interaction
    Tolga Dalman, Peter Droste, Michael Weitzel, Wolfgang Wiechert, and Katharina Nöh
  3. Intelligent Document Routing in SQL: a Case Study
    Carlos Soares and Miguel Calejo
  4. Combining Subgroup Discovery and Permutation Testing to Reduce Reduncancy
    Jeroen S. de Bruin and Joost N. Kok
  5. Semantically-guided Workflow Construction in Taverna – The SADI and BioMoby Plugins
    David Withers, Edward Kawas, Luke McCarthy, Benjamin Vandervalk, and Mark Wilkinson
  6. Workflow Construction for Service-Oriented Knowledge Discovery
    Vid Podpecan, Monika Zakova, and Nada Lavrac
  7. Workflow composition and enactment using jORCA
    Johan Karlsson, Victoria Martín-Requena, Javier Ríos, and Oswaldo Trelles
  8. 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)

Track Organizers

Visar Januzaj (TU Darmstadt)
Stefan Kugele (TU Muenchen)
Boris Langer (Diehl Aerospace)
Christian Schallhart (TU Darmstadt)
Helmut Veith (TU Wien)

Content

  1. New Challenges in the Development of Critical Embedded Systems - an "aeromotive" Perspective
    Visar Januzaj, Stefan Kugele, Boris Langer, Christian Schallhart, and Helmut Veith
  2. Certification of Embedded Software – Impact of ISO DIS 26262 in the Automotive Domain
    Bernhard Schätz
  3. 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
  4. Seamless Model-driven Development put into Practice
    Wolfgang Haberl, Markus Herrmannsdoerfer, Stefan Kugele, Michael Tautschnig, and Martin Wechs
  5. Timely Time Estimates
    Andreas Holzer, Visar Januzaj, Stefan Kugele, and Michael Tautschnig
  6. 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:

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

  1. Towards a Research Agenda for Enterprise Crowdsourcing
    Maja Vukovic and Claudio Bartolini
  2. Analyzing Collaboration in Software Development Processes through Social Networks
    Andréa Magalhães Magdaleno, Cláudia Maria Lima Werner, and Renata Mendes de Araujo
  3. A Web-based Framework for Collaborative Innovation
    Donald Cowan, Paulo Alencar, Fred McGarry, Carlos Lucena, and Ingrid Nunes
  4. A Distributed Dynamics for Web Graph Decontamination
    Vanessa C. F. Gonçalves, Priscila M. V. Lima, Nelson Maculan, and Felipe M. G. França
  5. 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
  6. Understanding IT Organizations
    Claudio Bartolini, Karin Breitman, Simone Diniz Junqueira Barbosa, Mathias Salle, Rita Berardi, Glaucia Melissa Campos, and Erik Eidt
  7. 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:

Track Organizers

Pierre-Loïc Garoche (ONERA)
Rémi Delmas (ONERA)

Content

  1. 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
  2. Analyzing the Security in the GSM Radio Network using Attack Jungles
    Parosh Aziz Abdulla, Jonathan Cederberg, and Lisa Kaati
  3. Formal Modeling and Verification of Sensor Network Encryption Protocol in the OTS/CafeOBJ Method
    Iakovos Ouranos, Petros Stefaneas, and Kazuhiro Ogata
  4. 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
  5. 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):

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

  1. A Scalable Approach for the Description of Dependencies in Hard Real-Time Systems
    Steffen Kollmann, Victor Pollex, Kilian Kempf, and Frank Slomka
  2. Verification of Printer Datapaths using Timed Automata
    Georgeta Igna and Frits Vaandrager
  3. 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
  4. Source-Level Support for Timing Analysis
    Gergö Barany and Adrian Prantl
  5. Practical Experiences of Applying Source-Level WCET Flow Analysis on Industrial Code
    Björn Lisper, Andreas Ermedahl, Dietmar Schreiner, Jens Knoop, and Peter Gliwa
  6. Worst-Case Analysis of Heap Allocations
    Wolfgang Puffitsch, Benedikt Huber, and Martin Schoeberl
  7. Partial Flow Analysis with oRange
    Marianne de Michiel, Armelle Bonenfant, Clément Ballabriga, and Hugues Cassé
  8. Towards an evaluation infrastructure for automotive multicore real-time operating systems
    Jörn Schneider and Christian Eltges
  9. Context-Sensitivity in IPET for Measurement-Based Timing Analysis
    Michael Zolda, Sven Bünte, and Raimund Kirner
  10. 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

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

  1. Quantitative Verification in Practice
    Boudewijn R. Haverkort, Joost-Pieter Katoen, and Kim G. Larsen
  2. 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
  3. Towards Dynamic Adaptation of Probabilistic Systems
    S. Andova, L.P.J. Groenewegen, and E.P. de Vink
  4. 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
  5. 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
  6. 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

  1. An Interface Algebra for Estimating Worst-Case Traversal Times in Component Networks
    Nikolay Stoimenov, Samarjit Chakraborty, and Lothar Thiele
  2. Towards resource-optimal routing plans for real-time traffic
    Alessandro Lori, Giovanni Stea, Gigliola Vaglini
  3. Partially synchronizing periodic flows with offsets improves worst-case end-to-end delay analysis of switched Ethernet
    Xiaoting Li, Jean-Luc Scharbarg, Christian Fraboul
  4. Analyzing end-to-end Functional Delays on an IMA Platform
    Michael Lauer, Jérôme Ermont, Claire Pagetti, Frédéric Boniol
  5. The PEGASE project: precise and scalable temporal analysis for aerospace communication systems with Network Calculus
    Marc Boyer, Nicolas Navet, Xavier Olive, and Eric Thierry
  6. NC-maude: a rewriting tool to play with network calculus
    Marc Boyer
  7. DEBORAH: A Tool for Worst-case Analysis of FIFO Tandems
    Luca Bisti, Luciano Lenzini, Enzo Mingozzi, and Giovanni Stea
  8. A Self-Adversarial Approach to Delay Analysis under Arbitrary Scheduling
    Jens B. Schmitt, Hao Wang, and Ivan Martinovic
  9. 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:

Track Organizers

He Jifeng (East China Normal University, Shanghai)
Zhiming Liu (UNU-IIST, Macao)
Abhik Roychoudhury (NUS, Singapore)

Content

  1. WOMM: A Weak Operational Memory Model
    Arnab De, Abhik Roychoudhury, and Deepak D’Souza
  2. A Memory Model for Static Analysis of C Programs
    Zhongxing Xu, Ted Kremenek, and Jian Zhang
  3. Analysing Message Sequence Graph Specifications
    Joy Chakraborty, Deepak D’Souza, and K Narayan Kumar
  4. Optimize Context-Sensitive Andersen-style Points-to Analysis by Method Summarization and Cycle-Elimination
    Li Qian, Zhao Jianhua, and Li Xuandong
  5. A Formal Analysis of the Web Services Atomic Transaction Protocol with UPPAAL
    Anders P. Ravn, Jiri Srba, and Saleem Vighio
  6. SPARDL: A Requirement Modeling Language for Periodic Control System
    Zheng Wang, Jianwen Li, Yongxin Zhao, Yanxia Qi, Geguang Pu, Jifeng He, and Bin Gu
  7. AutoPA: Automatic Prototyping from Requirements
    Xiaoshan Li, Zhiming Liu, Martin Schäf, and Ling Yin
  8. 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):

Track Organizers

Alan Wassyng (McMaster University, Canada)
Tom Maibaum (McMaster University, Canada)
Mark Lawford (McMaster University, Canada)

Content

  1. Certification of Software-Driven Medical Devices
    Mark Lawford, Tom Maibaum, and Alan Wassyng
  2. Arguing for Software Quality in an IEC 62304 Compliant Development Process
    Michaela Huhn and Axel Zechner
  3. Design Choices for High-Confidence Distributed Real-time Software
    Sebastian Fischmeister and Akramul Azim
  4. Trustable Formal Specification for Software Certification
    Dominique Méry and Neeraj Kumar Singh
  5. 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

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):

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

  1. Formal Languages and Methods for Designing and Verifying Complex Embedded Systems
    Yamine Ait Ameur, Frédéric Boniol, Dominique Mery, and Virginie Wiels
  2. Analyzing the Security in the GSM Radio Network using Attack Jungles
    Parosh Aziz Abdulla, Jonathan Cederberg, and Lisa Kaati
  3. Formal Modeling and Verification of Sensor Network Encryption Protocol in the OTS/CafeOBJ Method
    Iakovos Ouranos, Petros Stefaneas, and Kazuhiro Ogata
  4. 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
  5. 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

  1. 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
  2. On Handling Data in Automata Learning - Considerations from the CONNECT Perspective
    Falk Howar, Bengt Jonsson, Maik Merten, Bernhard Steffen, Sofia Cassel
  3. A Theory of Mediators for Eternal Connectors
    Paola Inverardi, Valérie Issarny, and Romina Spalazzese
  4. On-the-fly Interoperability through Automated Mediator Synthesis and Monitoring
    Antonia Bertolino, Paola Inverardi, Valérie Issarny, Antonino Sabetta, and Romina Spalazzese
  5. Dependability Analysis and Verification for Connected Systems
    Felicita Di Giandomenico, Marta Kwiatkowska, Marco Martinucci, Paolo Masci, and Hongyang Qu
  6. 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

  1. Introduction to the EternalS Track: Trustworthy Eternal Systems via Evolving Software, Data and Knowledge
    Alessandro Moschitti
  2. HATS: Highly Adaptable and Trustworthy Software using Formal Methods
    Reiner Hähnle
  3. SecureChange: Security Engineering for Lifelong Evolvable Systems
    Riccardo Scandariato and Fabio Massacci
  4. 3DLife: Bringing the Media Internet to Life
    Ebroul Izquierdo, Tomas Piatrik and Qianni Zhang
  5. LivingKnowledge: Kernel Methods for Relational Learning and Semantic Modeling
    Alessandro Moschitti
  6. Task Forces in the EternalS Coordination Action
    Reiner Hähnle
  7. Modeling and Analyzing Diversity - Description of EternalS Task Force 1
    Ina Schaefle
  8. Modeling and Managing System Evolution Description of EternalS Task Force 2
    Michael Hafner
  9. Self-adaptation and Evolution by Learning - Description of EternalS Task Force 3
    Richard Johansson
  10. 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)

»Home | »Call for Papers | »Committees | »Tracks | »Co-located Events | »Program | »Paper Submission | »General Information | »Registration | »Accommodation | »ISoLA |
powered by OSWD |