Especificação, Verificação e Teste de Sistemas Críticos
Specification, Verification, and Testing of Critical Systems
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.
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.
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
Acções do Documento