Abstract
The complexity inherent to concurrent systems can turn their development into a very complex and error-prone task. The use of formal languages like CSP and tools that support them simplifies considerably the task of developing such systems. This process, however, usually aims at reaching an executable program: a translation between the specification language and a practical programming language is still needed and is usually rather problematic. In this paper we present a translation framework and a tool, csp2hc, that implements it. This framework provides an automatic translation from a subset of CSP to Handel-C, a programming language that is similar to standard C, but whose programs can be converted to produce files to program an FPGA.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Burns, A., Wellings, A.: Concurrency in Ada, 2nd edn. Cambridge University Press, Cambridge (1997)
Arvind: Bluespec: A language for hardware design, simulation, synthesis and verification invited talk. In: MEMOCODE 2003, p. 249. IEEE Computer Society Press, Washington, DC, USA (2003)
Augustin, L.M., Luckham, D.C., Gennart, B.A., Huh, Y., Stanculescu, A.G.: Hardware Design and Simulation in VAL/VHDL. Kluwer Academic Publishers, Dordrecht (1991)
Back, R.-J., Sere, K.: Stepwise Refinement of Action Systems. In: Proceedings of the International Conference on Mathematics of Program Construction, 375th Anniversary of the Groningen University, pp. 115–138. Springer, London, UK (1989)
Brown, N., Welch, P.: An Introduction to the Kent C++CSP Library. In: Broenink, J.F., Hilderink, G.H. (eds.) Communicating Process Architectures 2003, pp. 139–156 (September 2003)
Carré, B., Garnsworthy, J.: Spark-an annotated ada subset for safety-critical programming. In: TRI-ADA 1990, pp. 392–402. ACM Press, New York (1990)
Cavalcanti, A.L.C., Sampaio, A.C.A., Woodcock, J.C.P.: A refinement strategy for Circus. Formal Aspects of Computing 15(2–3), 146–181 (2003)
Celoxica. Handel-C language reference manual, v3.0 (2002)
Formal Systems Ltd. FDR: User Manual and Tutorial, version 2.82 (2005)
Freitas, A., Cavalcanti, A.L.C.: Automatic Translation from Circus to Java. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol. 4085, pp. 115–130. Springer, Heidelberg (2006)
Gamma, E., Helm, R., Johnson, R., Vlissides, J.: Design patterns: elements of reusable object-oriented software. Addison-Wesley, Reading (1995)
Hilderink, G., Broenink, J., Vervoort, W., Bakkers, A.: Communicating Java threads. In: Andr{\’e} Bakkers, W.P. (ed.) A Concurrent Pascal Compiler for Minicomputers, University of Twente, Netherlands, vol. 50, pp. 48–76. IOS Press, Netherlands (1997)
Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs (1985)
Jones, G., Goldsmith, M.: Programming in occam 2. Prentice-Hall, Englewood Cliffs (1988)
Hinchey, M.G., Jarvis, S.A.: Concurrent Systems: Formal Development in CSP. McGraw-Hill, New York (1995)
McMillin, B., Arrowsmith, E.: CCSP-A Formal System for Distributed Program Debugging. In: Proceedings of the Software for Multiprocessors and Supercomputers, Theory, Practice, Experience, Moscow, Russia (September 1994)
Oliveira, M.V.M., Cavalcanti, A.L.C.: From Circus to JCSP. In: Davies, J., Schulte, W., Barnett, M. (eds.) ICFEM 2004. LNCS, vol. 3308, pp. 320–340. Springer, Heidelberg (2004)
Phillips, J.D., Stiles, G.S.: An Automatic Translation of CSP to Handel-C. In: East, I.R., Duce, D., Green, M., Martin, J.M.R., Welch, P.H. (eds.) Communicating Process Architectures 2004, pp. 19–38 (September 2004)
Raju, V., Rong, L., Stiles, G.S.: Automatic Conversion of CSP to CTJ, JCSP, and CCSP. In: Broenink, J.F., Hilderink, G.H. (eds.) Communicating Process Architectures 2003, pp. 63–81 (September 2003)
Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice-Hall Series in Computer Science. Prentice-Hall, Englewood Cliffs (1998)
Stepney, S.: CSP/FDR2 to Handel-C translation. Technical Report YCS-2002-357, Department of Computer Science, University of York (June 2003)
Welch, P.H.: Process oriented design for Java: concurrency for all. In: Arabnia, H.R. (ed.) Proceedings of the International Conference on Parallel and Distributed Processing Techniques and Applications, pp. 51–57. CSREA Press (June 2000)
Woodcock, J.C.P., Davies, J.: Using Z—Specification, Refinement, and Proof. Prentice-Hall, Englewood Cliffs (1996)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Oliveira, M., Woodcock, J. (2007). Automatic Generation of Verified Concurrent Hardware. In: Butler, M., Hinchey, M.G., Larrondo-Petrie, M.M. (eds) Formal Methods and Software Engineering. ICFEM 2007. Lecture Notes in Computer Science, vol 4789. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-76650-6_17
Download citation
DOI: https://doi.org/10.1007/978-3-540-76650-6_17
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-76648-3
Online ISBN: 978-3-540-76650-6
eBook Packages: Computer ScienceComputer Science (R0)