A program analysis framework for tccp based on abstract interpretation

作者:Comini Marco; Gallardo Maria del Mar; Titolo Laura; Villanueva Alicia*
来源:Formal Aspects of Computing, 2017, 29(3): 531-557.
DOI:10.1007/s00165-016-0409-8

摘要

The timed concurrent constraint language (tccp) is a timed extension of the concurrent constraint paradigm. tccp was defined to model reactive systems, where infinite behaviors arise naturally. In previous works, a semantic framework and abstract diagnosis method for the language have been defined. On the basis of that semantic framework, this paper proposes an abstract semantics that, together with a widening operator, is suitable for the definition of different analyses for tccp programs. The abstract semantics is correct and can be represented as a finite graph where each node represents a hypothetical (abstract) computational step of the program. The widening operator allows us to guarantee the convergence of the abstract fixpoint computation.

  • 出版日期2017-5

全文