@article {LV09b,
	title = {The tccp Interpreter},
	journal = {Electronic Notes in Theoretical Computer Science},
	volume = {258},
	number = {1},
	year = {2009},
	pages = {63{\textendash}77},
	abstract = {The Timed Concurrent Constraint Language (tccp in short) is a constraint-based concurrent language inspired in process algebra. The language is well-suited for the specification of concurrent and reactive systems. tccp is parametric w.r.t. a constraint system, what is a main characteristic of the Concurrent Constraint Paradigm of Saraswat. Maude is an executable rewriting logic language specially well suited for the specification of distributed systems. The tccpInterpreter system is the result of implementing the tccp language (the constraint system, agents and semantics) in Maude. It parses the program and mimics in an automatic way its behavior allowing us to use the Maude features to execute and analyze tccp programs.},
	author = {Lescaylle, A. and Alicia Villanueva}
}
@article {LV09,
	title = {A Tool for Generating a Symbolic Representation of tccp Executions},
	journal = {Electronic Notes in Theoretical Computer Science},
	volume = {246},
	year = {2009},
	pages = {131{\textendash}145},
	abstract = {
The Timed Concurrent Constraint language (tccp) was defined by F. de Boer et al. as an extension of the Concurrent Constraint Paradigm (Saraswat, 1993) for specifying reactive and embedded systems. In this paper, we describe the StructGenerator system which, given the specification of a tccp program, constructs a symbolic representation (a tccp Structure) modeling the behavior of such tccp program. The resulting structure allows one to verify the program by using a model-checking algorithm. It is similar to a Kripke Structure but, due to the nature of the ccp model, it differs from the classical approach in some important points that will be described along the paper. The StructGenerator system, implemented in C++, takes as input a file containing the specification of a tccp program and generates the associated tccp Structure. Along the paper, we cover the design and implementation of StructGenerator. We also demonstrate its functionality carrying out the execution of two practical examples.},
	author = {Lescaylle, A. and Alicia Villanueva}
}
@proceedings {LV07,
	title = {Using tccp for the Specification and Verification of Communication Protocols},
	journal = {Proceedings of the 16th International Workshop on Funcional and (Constraint) Logic Programming (WFLP{\textquoteright}07)},
	year = {2007},
	pages = {169{\textendash}183},
	address = {Paris (France)},
	abstract = {The automatic analysis of cryptographic protocols by using formal methods on concurrent languages is a subject widely treated in the literature. From its beginning in the decade of the 70s, the field has been gaining maturity and consolidation. Some declarative approaches based on CLP, Haskell or Maude have been proposed for the specification and analysis of communication protocols. In this paper, we propose the Timed Concurrent Constraint Language (tccp in short) as the specification language for protocols. tccp is a declarative concurrent programming language which allows one to intuitively model concurrent and reactive systems. Cryptographic protocols can be specified in a very compact way
thanks to certain features of the language such as the non-deterministic behavior and concurrency. We show how to specify the basic actions that are usually performed during a protocol run. Thereafter, we show how to specify the participants in the protocol. Finally, we specify the intruder model by means of a hostile environment in which principals run the protocol. The model considered for the intruder is the popular model of Dolev-Yao. We use along the paper the Needham-Schroeder public key authentication protocol to illustrate the approach. The basic actions and the intruder implementation can be reused for the specification of many different protocols.},
	keywords = {tccp},
	author = {Lescaylle, A. and Alicia Villanueva}
}
@proceedings {LV07b,
	title = {Using tccp for the Specification of Communication Protocols},
	journal = {Actas de las VII Jornadas de Programaci{\'o}n y Lenguajes (PROLE{\textquoteright}07)},
	year = {2007},
	pages = {301{\textendash}310},
	address = {Zaragoza (Spain)},
	abstract = {The automatic analysis of cryptographic protocols by using formal methods on concurrent languages is a subject widely treated in the literature. From its beginning in the decade of the 70s, the field has been gaining maturity and consolidation. The Timed Concurrent Constraint Language (tccp in short) is a declarative concurrent programming language which, like other concurrent languages, allows us to intuitively model concurrent and reactive systems. In particular, cryptographic protocols can be specified in a very compact way thanks to certain features such as the non-determinism and concurrency, which are necessary to model such kind of systems. In this work, we show a method to specify cryptographic protocols using tccp. We have defined specifications for the actions that principals usually do during a protocol run. Moreover, we have defined a hostile environment in which agents run the protocol. The environment is actually the representation of the popular intruder model of Dolev-Yao. We use the Needham-Schroeder public key authentication protocol to illustrate the approach.},
	author = {Lescaylle, A. and Alicia Villanueva}
}
