Especificação, Verificação e Teste de Sistemas Críticos

Specification, Verification, and Testing of Critical Systems

EVTSIC’10

 Scope

Critical systems are those for which some aspect of their functioning must be preserved under all circumstances – failure may have unacceptable consequences such as the loss of human lives, the destruction of expensive equipment, or leakage of classified information.

Some (non-disjoint) classes of critical software are:

• Safety-critical systems, for which a set of situations is identified whose occurrence is forbidden. Typically associated with program execution errors (e.g. overflow).

• Business-critical systems, whose functioning is vital to the economic goals of an organisation.

• Mission-critical systems, associated to the execution of some mission that must absolutely not fail (for instance in the military or space context).

• Security-critical systems, that manipulate information whose integrity or confidentiality must be preserved at all costs.

• Embedded and real-time systems, that control mechanisms in the physical world subject to additional specific requirements, such as timing or resource-availability (in the hosting mechanism) requirements.

The goal of this track is to bring together researchers from the critical software community, together with researchers working in rigorous development of software, to foster collaboration and to address the growing demand for the application of so-called formal methods in the critical systems arena. Cross-fertilisation between theory and practice is the main focus of the track, but both fundamental work and industry experience reports are welcome.

Topics

We solicit original papers on all topics related to the specification, verification, and testing of critical systems, as well as to formal approaches to software development in general. This includes among others

• Formalisms for specifying the behaviour of critical systems, in particular specifying safety requirements and requirements of embedded and real-time systems;

• Formal verification techniques: model-checking; deductive program verification; verification of concurrent and real-time systems;

• Techniques associated to the formal study of programming languages; language-based security; language-based verification techniques;

• Approaches to testing of critical systems; model-based testing;

• Other techniques: static analysis; theorem proving; semi-formal modeling techniques;

• Case studies: detailed accounts of the application of a technique, method, or toolset in the context of critical development;

• Industry experience papers: detailed reports of critical system design and development, or of the application of formal methods in the industrial context.

Submission and Publication

Submissions to the track will be judged on the basis of originality, relevance, technical soundness and presentation quality. Papers must be written in Portuguese or English and not exceed 12 pages in LNCS format. Papers should be submitted electronically via the web-based submission site. If you experience any problems with the submission procedure please contact the PC chair.

Publication of the (English-language) revised proceedings in an international electronic journal is under negotiation.

Program Committee

Sérgio Amado, EDISOFT

Nestor Cataño, UNIV. MADEIRA

José Miguel Faria, CRITICAL SOFTWARE

Carla Ferreira, UNIV. NOVA LISBOA

Mário Florido, UNIV. PORTO

Ana Matos, UNIV. TÉCNICA LISBOA

Nelma Moreira, UNIV. PORTO

Ana Paiva, UNIV. PORTO

Luís Miguel Pinho, INST.SUP.ENG. PORTO

Luís Pinto, UNIV. MINHO

Jorge Sousa Pinto, UNIV. MINHO (chair)

Simão Melo de Sousa, UNIV. B. INTERIOR

Contacts:

jsp<at>di<dot>uminho<dot>pt