A temporal logic is presented for reasoning about the correctness of timed concurrent constraint programs. The logic is based on modalities which allow one to specify what a process produces as a reaction to what its environment inputs. These modalities provide an assumption/commitment style of specification which allows a sound and complete compositional axiomatization of the reactive behavior of timed concurrent constraint programs. Categories and Subject Descriptors: D.3.2 [Programming Languages]: Language Classifications— Constraint and logic languages; F.1.2 [Computation by Abstract Devices]: Modes of Computation—Interactive and reactive computation; F.3.1 [Logics and Meanings of Programs]: Specifying and Verifying and Reasoning about Programs—Logics of programs; F.4.1 [Mathematical Logic and Formal Languages]: Mathematical Logic—Temporal logic General Terms: Languages, Verification Additional Key Words and Phrases: Concurrency, constraints, reactive systems, temporal logic

Proving correctness of timed concurrent constraint programs

MEO, MARIA CHIARA
2004-01-01

Abstract

A temporal logic is presented for reasoning about the correctness of timed concurrent constraint programs. The logic is based on modalities which allow one to specify what a process produces as a reaction to what its environment inputs. These modalities provide an assumption/commitment style of specification which allows a sound and complete compositional axiomatization of the reactive behavior of timed concurrent constraint programs. Categories and Subject Descriptors: D.3.2 [Programming Languages]: Language Classifications— Constraint and logic languages; F.1.2 [Computation by Abstract Devices]: Modes of Computation—Interactive and reactive computation; F.3.1 [Logics and Meanings of Programs]: Specifying and Verifying and Reasoning about Programs—Logics of programs; F.4.1 [Mathematical Logic and Formal Languages]: Mathematical Logic—Temporal logic General Terms: Languages, Verification Additional Key Words and Phrases: Concurrency, constraints, reactive systems, temporal logic
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11564/109536
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 7
  • ???jsp.display-item.citation.isi??? ND
social impact