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 logicI documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.