FESCA Workshop at ETAPS'04: First Call for Papers

                        *** FIRST CALL FOR PAPERS  ***

                                 FESCA 2004

   1st International Workshop on Formal Foundations of Embedded Software and 
                     Component-Based Software Architectures

                     http://www.csse.monash.edu.au/fesca/
 
                       Satellite event of ETAPS 2004
                          27 March - 4 April 2004, 
                        Barcelona, Catalonia, Spain
                       http://www.lsi.upc.es/etaps04/

The aim of this ETAPS 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. 

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, this trend has been amplified. Various 
component models, models of computation and component composition techniques 
and frameworks have been proposed in the literature. 

An underlying theme of all these is to establish correctness or correct by 
construction software engineering. 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. In fact, software complexity 
is increasing at a pace greater than Moore's law due to the use of software in 
many facets of computation such as multi-media, real-time systems, networking 
protocol stacks, complex/real-time operating systems, networked systems 
software, pervasive networking, etc. 

Ubiquitous computing is envisioned as the nature of computation in the 
near future as evidenced in the emergence of various middleware enabled 
ubiquitous systems software, such as JINI, .NET, CORBA etc. A quantum leap 
in the formal methodology and tools is needed to cope with this rising 
software complexity, or else, correctness guarantees will remain forever 
elusive. Component software technology gives us some hope because of its 
inherent 'divide and conquer' nature. However, complex interactions between 
components pose greater challenges as well. Middleware platforms have 
proposed a variety of component models (such as OMG's CORBA or implementations
of Sun Microsystems's EJB or Microsoft's .NET). Similarly, meta-models have 
been developed and standardized to specify component-based software 
architectures (e.g. UML2.0 or the UML Profile for Enterprise Distributed 
Object Computing). Also, many embedded software industries (e.g. in avionics) 
have either in-house or application specific design flows or middleware 
(e.g. ARINC/APEX rtos API standard for avionics). These approaches provide 
the ability to clearly model and organize components into architectures. 
However, formal analysis and reasoning is gaining ever increasing importance 
due to application of software in critical applications. Many such 
applications ranging from bio-medical devices to sophisticated weapons 
systems are designed from components. 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. 

Topics

We encourage submissions on formal techniques that aid reasoning, analysis and 
certification of embedded software and component-based software architectures. 

In this context the following topics are of particular concern: 
* component interoperability, 
* contractually used components, 
* interface compliancy (interface-to-interface and 
interface-to-implementation), 
* compliancy with synchronization constraints, 
* temporal properties including liveness and safety, 
* security/access rights, further non-functional properties (reliability, 
performance, timeliness), 
* formal methods and dependability,
* formal design methodologies and modeling techniques, 
* formal methods for embedded real-time software, 
* formal methods and pervasive computing. 

Tools and techniques might involve (but are not limited to): 
* logic-based approaches using interactive or automated theorem proving (e.g., 
B, Z, PVS, 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.

Submissions

Submissions of short papers (no longer than 2 pages) or full papers (no longer
than 10 pages) 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 the workshop email address 
fesca-04-9iOJEv++55WdZ29H/IFGnA@xxxxxxxxxxxxxxxx All valid submissions will be 
reviewed by at 
least two members of the program committee. The acceptance of a submission 
implies the registration and attendance of at least one of the authors to 
the workshop.

Publication

Final versions of accepted papers will be included in an informal workshop 
proceedings. A special volume of "Component Based Software for Embedded 
Systems" with selected papers from the workshop is planned, with Kluwer 
Academic Publishers as a possible publisher. A special issue of one of the 
leading journals of embedded systems based on select papers at the workshop 
is also being considered.

Important Dates 

Submission deadline: 14th December 2003
Notification of acceptance/rejection: 19th January 2004
Final version: 15th February 2004
Workshop: 3rd April 2004 

Organizers

* Juliana Küster Filipe, jkfilipe-9iOJEv++55WFxr2TtlUqVg@xxxxxxxxxxxxxxxx, 
University of Edinburgh, UK 
* Iman H. Poernomo, ihp-U9WltOpzlwvGkZ5O/9TfLxCuuivNXqWP@xxxxxxxxxxxxxxxx, 
Monash University, Australia 
* Ralf H. Reussner, 
Reussner-jNDFPZUTrfTUvfpBxBsQfasoZZ7OtMbqG9Ur7JDdleE@xxxxxxxxxxxxxxxx, 
University of Oldenburg, Germany
* Sandeep K. Shukla, shukla-PjAqaU27lzQ@xxxxxxxxxxxxxxxx, Electrical and 
Computer Engineering, Virginia Tech, USA

Program Committee

* Angelo Corsaro (University of California at Irvine, USA) 
* Frederic Doucet (University of California at Irvine, USA) 
* Paul Le Guernic (IRISA/INRIA, France) 
* Rajesh K. Gupta (University of California, San Diego, USA) 
* Juliana Küster Filipe (University of Edinburgh, UK) 
* Chris Ling (Monash University, Australia)
* Seng Loke (Monash University, Australia)
* Iman H. Poernomo (Monash University, Australia) 
* Ralf H. Reussner (University of Oldenburg, Germany) 
* Sandeep K. Shukla (Virginia Tech, USA)
* Jean-Pierre Talpin (IRISA/INRIA, France) 
* Alexandre Zamulin (A.P.Ershov Institute of Informatics Systems, Russia)




--------------------------------------------------------------------------
To subscribe or unsubscribe yourself from
dbworld, send a msg to majordomo-hcNo3dDEHLuVc3sceRu5cw@xxxxxxxxxxxxxxxx with 
one of these lines:
subscribe dbworld OR unsubscribe dbworld
To find out more options send a msg with the line:
help
To post messages, go to URL www.cs.wisc.edu/dbworld
--------------------------------------------------------------------------