×

A denotational semantics for Handel-C. (English) Zbl 1216.68154


MSC:

68Q55 Semantics in the theory of computing
68N15 Theory of programming languages

Software:

Haskell; Handel-C; Circus
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Abdallah AE, Hawkins J (2003) Formal behavioural synthesis of Handel-C parallel hardware implementations from functional specifications. In: 36th annual Hawaii international conference on system sciences (HICSS’03). IEEE
[2] Andriessens C, Lindner T (1996) AL: using FOCUS, LUSTRE, and probability theory for the design of a reliable control program. Lect Notes Comput Sci 1165: 35–51
[3] Bravetti M, Gorrieri R (2000) A complete axiomatization for observational congruence of prioritized finite-state behaviors. In: Montanari U, Rolim JDP, Welzl E (eds) Proceedings of the 27th international colloquium on automata, languages and programming, ICALP 2000, Geneva, Switzerland, July 9–15, 2000. Lecture notes in computer science, vol 1853. Springer, Berlin, pp 744–755 · Zbl 0973.68168
[4] Björner D, Jones CB (1982) Formal specification & software development. Prentice-Hall, Englewood Cliffs
[5] Bjørner D (2004) TRain: the railway domain–A ”grand challenge” for computing science & transportation engineering. In: Jacquart R (eds) IFIP Congress Topical Sessions. Kluwer, Dordrecht, pp 607–612
[6] Bjørner D (2006) Software engineering, vol. 3: Domains, requirements and software design. Texts in theoretical computer science. Springer, Berlin
[7] Bouali A (1998) Xeve: an Esterel verification environment. Lect Notes Comput Sci 1427: 500–504
[8] Brookes SD (1985) On the axiomatic treatment of concurrency. Lect Notes Comput Sci 197: 1–34
[9] Boussinot F, De Simone R (1991) The ESTEREL language. Technical Report RR-1487, Inria, Institut National de Recherche en Informatique et en Automatique
[10] Butterfield A, Sherif A, Woodcock J (2007) Slotted-Circus–a UTP-Family of Reactive Theories. In: Davies J, Gibbons J (eds) IFM 2007. Lecture notes in computer science, vol 4591. Springer, Berlin
[11] Butterfield A (2001) Denotational semantics for prialt-free Handel-C. Technical Report TCD-CS-2001-53, Dept. of Computer Science, Trinity College, Dublin University
[12] Butterfield A (2001) Interpretative semantics for prialt-free Handel-C. Technical Report TCD-CS-2001-54, Dept. of Computer Science, Trinity College, Dublin University
[13] Butterfield A (2007) A denotational semantics for Handel-C. In: Jones CB, Liu Z, Woodcock J (eds) Formal methods and hybrid real-time systems. Lecture notes in computer science, vol 4700. Springer, Berlin, pp 45–66 · Zbl 1151.68346
[14] Butterfield A, Woodcock J (2002) Semantic Domains for Handel-C. In: Madden N, Seda A (eds) Mathematical foundations for computer science and information technology (MFCSIT 2003). Electronic notes in theoretical computer science, vol 74. http://www.elsevier.nl/locate/entcs (to appear)
[15] Butterfield A, Woodcock J (2002) Semantics of prialt in Handel-C. In: Pasco J, Welch P, Loader R, Sunderam V (eds) Communicating process architectures 2002. Concurrent systems engineering. IOS Press, Amsterdam, pp 1–16
[16] Butterfield A, Woodcock J (2003) An operational semantics for Handel-C. In: Arts T, Fokkink W (eds) Electronic notes in theoretical computer science, vol 80. Elsevier, Amsterdam · Zbl 1270.68151
[17] Butterfield A, Woodcock J (2005) prialt in Handel-C: an operational semantics. Int J Softw Tool Technol Transf (STTT) 7(3): 248–267. doi: 10.1007/s10009-004-0181-6 · doi:10.1007/s10009-004-0181-6
[18] Butterfield A, Woodcock J (2006) A ”hardware compiler” semantics for Handel-C. Electr Notes Theor Comput Sci 161: 73–90 · doi:10.1016/j.entcs.2006.04.026
[19] Celoxica Ltd (2002) Handel-C Language Reference Manual, v3.0. URL: http://www.celoxica.com
[20] Cleaveland R, Hennessy M (1990) Priorities in process algebras. Inf Comput 87(1/2): 58–77 · Zbl 0726.68053 · doi:10.1016/0890-5401(90)90059-Q
[21] Coutinho JGF, Luk W (2003) Source-directed transformations for hardware compilation. In: Proceedings of the field-programmable technology (FPT), pp 278–285
[22] Cleaveland R, Lüttgen G, Natarajan V (2007) Priority and abstraction in process algebra. Inf Comput 205(9): 1426–1458 · Zbl 1127.68067 · doi:10.1016/j.ic.2007.05.001
[23] Corcoran BJ (2005) Testing formal semantics: Handel-C. M.Sc. in Computer Science, University of Dublin, Trinity College, September 2005. presented in partial fullfillment of the M.Sc. requirements
[24] Camilleri J, Winskel G (1995) CCS with priority choice. Inf Comput 116(1): 26–37 · Zbl 0818.68107 · doi:10.1006/inco.1995.1003
[25] Damianou N, Dulay N, Lupu E, Sloman M (2001) The Ponder policy specification language. Lect Notes Comput Sci 1995: 18–38
[26] Fidge CJ (1993) A formal definition of priority in CSP. ACM Trans Program Lang Syst 15(4): 681–705 · doi:10.1145/155183.155221
[27] Gancarski P, Butterfield A (2009) The denotational semantics of slotted-circus. In: Cavalcanti A, Dams D (eds) FM2009: Formal methods. LNCS, vol 5850. Springer, Berlin, pp 451–466
[28] Hoare CAR, Jifeng H (1998) Unifying theories of programming. Series in computer science. Prentice Hall, Englewood Cliffs
[29] Hermanns H, Lohrey M (1998) Priority and maximal progress are completely axiomatisable. Lect Notes Comput Sci 1466: 237–252 · Zbl 0940.68054
[30] Hoare CAR (1985) Communicating sequential processes. International series in computer science. Prentice Hall, Englewood Cliffs
[31] Holenderski L (1995) LUSTRE. In: Lewerentz C, Lindner T (eds) Formal development of reactive systems, case study production cell. Lecture notes in computer science. Springer, Berlin, pp 101–112
[32] Jones SP et al (1999) Report on the programming language Haskell 98. http://www.haskell.org/
[33] Lawrence AE (2001) CSPP and event priority. In: Mirmehdi M, Chalmers A, Muller H (eds) Communicating process architectures 2001. Concurrent systems engineering. IOS Press, Amsterdam
[34] Lawrence AE (2002) Acceptances, Behaviours and infinite activity in CSPP. In: Communicating process architectures 2002. Concurrent systems engineering. IOS Press, Amsterdam
[35] Lawrence AE (2002) HCSP and true concurrency. In: Communicating process architectures 2002. Concurrent systems engineering. IOS Press, Amsterdam
[36] Lowe G (1993) Probabilities and priorities in timed CSP. PhD thesis, Oxford University
[37] Lee H, Yusuf S, Luk W, Sloman M, Lupu E, Dulay N (2002) Development framework for firewall processors. In: IEEE international conference on field-programmable technology (FPT), Chinese University of Hong Kong, New Territories, Peoples Republic of China. http://pubs.doc.ic.ac.uk/DevelopmentFirewall/
[38] Mícheál (1991) Mac an Airchinnigh. The Irish School of VDM. In: VDM ’91. Lecture notes in computer science, vol 552. Springer, Berlin
[39] Page I (1996) Constructing of hardware–software systems from a single description. J VLSI Signal Process 12(1):87–107. http://dx.doi.org/10.1007/BF00936948
[40] Phillips I (2008) CCS with priority guards. J Log Algebr Program 75(1): 139–165 · Zbl 1134.68042 · doi:10.1016/j.jlap.2007.06.005
[41] Page I, Luk W (1991) Compiling occam into field-programmable gate arrays. In: Moore W, Luk W (eds) FPGAs, Oxford workshop on field programmable logic and applications. Abingdon EE&CS Books, Abingdon, pp 271–283
[42] Perna J, Woodcock J (2010) UTP semantics for Handel-C. In: Butterfield A (ed) 2nd international symposium on unifying theories of programming, vol 5713 (page to appear) · Zbl 1286.68035
[43] Tini S (2001) An axiomatic semantics for Esterel. TCS: theoretical computer science, vol 269 · Zbl 0983.68136
[44] Woodcock J, Cavalcanti A (2002) The semantics of Circus. LNCS, vol 2272. 2nd International Conference of B and Z Users, Grenoble, France, Springer · Zbl 1044.68560
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.