Anzeige
Erschienen in:
2013 | OriginalPaper | Buchkapitel
A CSP Timed Input-Output Relation and a Strategy for Mechanised Conformance Verification
verfasst von : Gustavo Carvalho, Augusto Sampaio, Alexandre Mota
Erschienen in: Formal Methods and Software Engineering
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
Here we propose a timed input-output conformance relation (named CSPTIO) based on the process algebra CSP. In contrast to other relations, CSPTIO analyses data-flow reactive systems and conformance verification is mechanised in terms of a high-level strategy by reusing successful techniques and tools: refinement checking (particularly, using the FDR tool) and SMT solving (using Z3). Therefore, conformance verification does not require the implementation of specific algorithms or the manipulation of complex data structures. Furthermore, the mechanisation is proved sound. To analyse the usefulness of CSPTIO, we first consider a toy example. Then we analyse critical systems from two different domains: aeronautics and automotive. CSPTIO detected all undesired behaviours in the analysed implementation models.