Abstract
In this paper we present the affine clock calculus as an extension of the formal verification techniques provided by the Signal language. A Signal program describes a system of clock synchronisation constraints the consistency of which is verified by compilation (clock calculus). Well-adapted in control-based system design, the clock calculus has to be extended in order to enable the validation of signal-alpha applications which usually contain important numerical calculations. The new affine clock calculus is based on the properties of affine relations introduced between clocks by the refinement of signal-alpha specifications in a codesign context. Affine relations enable the derivation of a new set of synchronisability rules which represent conditions against which synchronisation constraints on clocks can be assessed. Properties of affine relations and synchronisability rules are derived in the semantical model of traces of signal. A prototype implementing a subset of the synchronisability rules has been integrated in the signal compiler and used for the validation of a video image coding application specified using signal and alpha.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Amagbegnon T., Besnard L., Le Guernic P.: Arborescent Canonical Form of Boolean Expressions. INRIA Research Report 2290, IRISA/INRIA-Rennes, France, 1994
Amagbegnon T., Le Guernic P., Marchand H., Rutten E.: The Signal dataflow methodology applied to a production cell. IRISA Research Report 917, IRISA/INRIA-Rennes, France, 1995
Belhadj M.: “Using Vhdl for Link to Synthesis Tools”. Proceedings of the North Atlantic Test Workshop, June 1994, Nmes, France
Benveniste A., Berry G.: “Real-Time systems design and programming”, Proceedings of the IEEE, September 1991, 79, (9)
Besnard L.: Compilation de Signal: horloges, dpendances, environnement, PhD Thesis, University of Rennes 1, France, September 1992
Birkoff G.: Lattice Theory, AMS colloquium publications, 1973.
De Micheli G.: “Computer-Aided Hardware-Software Codesign”, IEEE Micro, August 1994, 14, (4)
ETSI (European Telecommunication Standards Institute) Specification of Component TV codecs 32-45 Mbit/s. December 1990
Gautier T., Le Guernic P., Quinton P., Rajopadhye S., Risset T., Smarandache I.: “Projet CAIRN: conception d’architectures partir de Signal et Alpha” CODESIGN Conception conjointe logiciel-matriel, Eyrolles, Collection Technique et Scientifique des Tlcommunications, 1998
Gupta R.K., Coelho C.N., De Micheli G.: “Program Implementation Schemes for Hardware-Software Systems” Computer, January 1994, pp. 48–55
Kalavade A., Lee E.A.: “A Hardware-Software Codesign Methodology for Dsp Applications” IEEE Design & Test of Computers, September 1993, 10, (3), pp. 16–28
Le Guernic P., Gautier T.: “Data-Flow to von Neumann: the Signal Approach”, Advanced Topics in Data-Flow Computing, (Gaudiot J. L. and Bic L., 1991), pp. 413–438
Le Guernic P., Gautier T., Le Borgne M., Le Maire C.: “Programming Real-time Applications with Signal”, Proceedings of the IEEE, September 1991, 79, (9), pp. 1321–1336
Salinas M.H., Johnson B.W., Aylor J.H.: “Implementation-Independent Model of an Instruction Set Architecture in Vhdl” IEEE Design & Test of Computers, September 1993, 10, (3), pp. 42–54
Sanderson J.G.: A Relational Theory of Computing, Springer Verlag 1980, 80, Goss G. and Hartmanis J.
Smarandache I.: Transformations affines d’horloges: application au codesign de systèmes temps-réel en utilisant les langages Signal et Alpha, PhD Thesis, University of Rennes 1, France, October 1998
Smarandache I. Le Guernic P.: “Affine Transformations in Signal and Their Applications in the Specifications and Validation of Real-Time Systems” Transformation-Based Reactive Systems Development, Proceedings of the 4th International AMAST Workshop on Real-Time Systems and Concurrent and Distributed Software, Palma, Spain, LNCS 1231, Springer Verlag, 1997
Smarandache I., Le Guernic P.: A Canonical Form for Affine Relations in Signal. INRIA Research Report 3097, IRISA/INRIA-Rennes, France, 1997
Thomas D.E., Adams J.K., Schmit H.: “A Model and Methodology for Hardware-Software Codesign” IEEE Design & Test of Computers, September 1993, 10, (3), pp. 6–15
Wilde D.: The Alpha Language. IRISA Research Report 827, IRISA/INRIA-Rennes, France, 1994
Wilde D., Sié O.: Regular array synthesis using Alpha. IRISA Research Report 829, IRISA/INRIA-Rennes, France, 1994
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Smarandache, I.M., Gautier, T., Le Guernic, P. (1999). Validation of mixed signal-alpha real-time systems through affine calculus on clock synchronisation constraints. In: Wing, J.M., Woodcock, J., Davies, J. (eds) FM’99 — Formal Methods. FM 1999. Lecture Notes in Computer Science, vol 1709. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48118-4_22
Download citation
DOI: https://doi.org/10.1007/3-540-48118-4_22
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66588-5
Online ISBN: 978-3-540-48118-8
eBook Packages: Springer Book Archive