Validating Component Integration with C-TILCO | Zendy

Pierfrancesco Bellini | Zendy; Paolo Nesi | Zendy; Davide Rogai | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

Validating Component Integration with C-TILCO

Author(s) -

Pierfrancesco Bellini,

Paolo Nesi,

Davide Rogai

Publication year - 2005

Publication title -

electronic notes in theoretical computer science

Language(s) - English

Resource type - Journals

SCImago Journal Rank - 0.242

H-Index - 60

ISSN - 1571-0661

DOI - 10.1016/j.entcs.2004.02.080

Subject(s) - computer science , temporal logic , executor , mathematical proof , component (thermodynamics) , implementation , property (philosophy) , programming language , temporal logic of actions , extension (predicate logic) , linear temporal logic , theoretical computer science , interval temporal logic , mathematics , philosophy , physics , geometry , epistemology , political science , law , thermodynamics

Temporal logics are typically used to specify and verify properties and thus requirements, to describe the system and to prove whether such formalization meets the expected behavior. In this paper, C-TILCO temporal logic is considered. C-TILCO is an extension of TILCO temporal logic which provides compositional and communication primitives. TILCO specifications of system behavior can be directly used as implementations since they can be directly executed in real-time by using the TILCO executor. The validation phase can be applied to both the single components and their integration in order to validate the entire solution. In this article, a case study about specification of a communicating system is presented together with some important property proofs taken from the validation phase

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research