FESCA @ ETAPS:

Formal Foundations of Embedded Software and Component-Based Software Architectures

Satellite workshop of ETAPS, the 29th of March 2008, Budapest, Hungary

The aim of this workshop is to bring together researchers from academia and industry interested in formal modeling approaches as well as associated analysis and reasoning techniques with practical benefits for embedded software and component-based software engineering.

2007 Preproceedings

The preproceedings of the 2007 workshop are available here. A final version will appear as a volume in the ENTCS series.

Workshop aim

Component-based software design has received considerable attention in industry and academia since object-oriented software development approaches became popular. Recent years has seen the emergence of formal and informal techniques and technologies for the specification and implementation of component-based software architectures. With the growing need for safety-critical embedded software and the increased relevance of reliability and scalability for enterprise software, this trend has been amplified.

Formal methods have sometimes not kept up with the increasing complexity of software. For instance, a range of new middleware platforms have been developed in both enterprise and embedded systems industries. Often, engineers use semi-formal notations such as UML2 to model and organize components into architectures.

FESCA aims to address the open question of how formal methods can be applied effectively to these new contexts and challenges. FESCA therefore is interested in formal methods known from the area of embedded software development and software engineering and tries to cross-fertilize their research and application.

Workshop topics

An underlying theme of formal methods research is to establish correctness or correct by construction. It is widely believed that formal methods are a good means to achieve correctness in complex software systems. However, advances in formal methods and formal verification have not kept up with the increasing complexity of software. We solicit papers that address this open problem.

One strength of FESCA is the link established between the embedded software design community and the formal software engineering community by exploring how formal approaches developed within one community affect or can be exploited by the other.

Previous FESCA workshops achieved this by looking at new computing paradigms like ubiquity, component-orientation and novel middleware technologies, which are of shared interest for both, embedded software design and formal software engineering.

FESCA 2007 will focus on other areas of shared interest:

(a) Dependability: Due to safety-requirements common for many embedded systems, dependability research is often concerned with embedded software controling technical systems. However, the demonstration of the dependability of a system is of increasing relevance also for enterprise software, as increasingly mission-critical enterprise systems and e-Commerce rely on software support.

(b) Quality attributes and resource consumption: in both domains, embedded and enterprise software, quality attributes gain an increasing interest. While current software development processes, as used in industry, are mainly driven by the correct implementation of functional requirements, the systematic evaluation and prediction of quality attributes such as reliability, availability, resource consumption, performance and scalability is a matter of research. We consider formalisms used in one of the domains of embedded or enterprise software to be useful for the other. Given the complexity of today's concurrent, distributed and networked software, it is extremely important to provide formal techniques and CASE tools for analysis and reasoning on local component properties as well as on global system properties.

We encourage submissions on formal techniques that aid reasoning, analysis and certification of component-based embedded software and enterprise software. In this context the following topics are of particular concern:

  • Contractually used components,
  • Interface compliancy (interface-to-interface and interface-to implementation),
  • Model driven approaches
  • Temporal properties including liveness and safety,
  • Software quality attributes (reliability, performance, timeliness) and resource consumption,
  • Formal methods and dependability
  • Runtime management of applications
  • Instrumentation and monitoring approaches
  • Tools and techniques might involve (but are not limited to): logic-based approaches using interactive or automated theorem proving (e.g., B, Z, PVS, Nuprl, Coq), concurrency models (e.g., process calculi, refinement calculi, state machines, Petri-nets), type theory based reasoning of correctness, component composition frameworks.

Submissions concentrating on specification techniques should involve an evaluation of the practical merit of their research and clearly state the analysis and reasoning techniques they enable. We also encourage work of a formal nature with immediate value to the industrial context.

History of FESCA

The previous FESCA workshops at ETAPS 2004, 2005, 2006 and 2007 were very successful events attracting submissions of high quality and participation of several respected researchers. It is expected that FESCA at ETAPS 2008 will make an equally positive contribution.

Papers accepted at previous FESCAs have been of exceptional standard, great timeliness and relevance to the workshop objectives. The workshop attracted guest speakers of international reputation in embedded systems and formal software engineering. Previous invited speakers have included been Constance L. Heitmeyer (Naval Research Laboratory, USA), Manfred Broy, (Technische Universitaet Muenchen, Germany), Jose Luiz Fiadeiro, (University of Leicester, UK), Frantisek Plasil (Charles University, Czech Republic) and Martin Wirsing (LMU, Germany).

Publication

Final versions of long accepted papers will be published in a special issue of the Electronic Notes in Computer Science (ENTCS). Authors of accepted short papers will have the opportunity to submit expanded versions of their papers for a second round of review for publication in the special issue. Short papers will not be included in the final proceedings.

Organizing Committee

Juliana Kuester Filipe Bowles, J.Kuester-Filipe `at symbol' cs.bham.ac.uk, School of Computer Science, University of Birmingham, UK

Iman Poernomo, iman.poernomo `at symbol' kcl.ac.uk, King's College London, UK

Ralf Reussner, reussner `at symbol' ipd.uka.de, University of Karlsruhe, Germany

Dates

Submission deadline for papers: February 1, 2008

Notification of acceptance/rejection: February 11, 2008

Final versions due: February 20, 2008

Workshop date: March 29, 2008

Submissions

Two kinds of papers submission are considered: short (between 2-4 pages) and long (longer than 10 pages) papers. Submissions should include author's full name(s), affiliation(s) and address(es), phone- and fax-number(s) and email address(es). Papers in PS or PDF-format should be emailed to iman.poernomo `at symbol' kcl.ac.uk. All valid submissions will be reviewed by at least two members of the program committee.

Programme committee

Samik Basu, Iowa State University, USA

Kenneth Chan, King's College London, UK

Martin Fraenzle, University of Oldenburg, Germany

Sabine Glesner, TU Berlin, Germany

Juliana Kuester Filipe Bowles (chair), University of Birmingham, UK

Sea Ling, Monash University, Australia

Julia Padberg, TU Berlin, Germany

Iman Poernomo (chair), King's College London, UK

Ralf Reussner (chair), University of Karlsruhe, Germany

Partha Roop, University of Auckland, New Zealand

Heinz Schmidt, Monash University, Australia

Heike Wehrheim, University of Paderborn, Germany

 




Supported by: