Abstract
The complexity of development and analysis is inherent to systems in general, especially in concurrent systems. When working with critical systems this becomes much more evident, as inconsistencies are usually associated with a high cost. Thus, the sooner we can identify an inconsistency in the design of a system and remove it, the lower its cost. For this reason, it is common to use strategies to reduce the difficulty and problems faced in this process. One of these strategies is the use of formal methods, which can, for instance, make use of process algebras to specify and analise concurrent systems, improving its understanding and enabling the identification of eventual concurrency problems and inconsistencies even in the initial stages of the project, ensuring the accuracy and correction of the system specification. This article presents a strategy for automatically translating the main operators of the process algebra CSP (Communicating Sequential Processes) into the VHSIC hardware description language (VHDL). The former is a language that allows us to make a formal description of a concurrent system and the latter is a hardware description language that can be compiled on a Field Programmable Gate Arrays (FPGA) board. Our automatic translator is validated by a case study of a smart elevator control system. We present its formal specification in CSP and then its translation into VHDL code, generated by our tool, which we synthesised on an FPGA board.
This work is partially supported by INES, CNPq grant 465614/2014-0, CAPES grant 88887.136410/2017-00, FACEPE grants APQ-0399- 1.03/17 and PRONEX APQ/0388-1.03/14.
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
Similar content being viewed by others
References
Burns, A., Wellings, A.: Concurrency in ADA, 2nd edn. Cambridge University Press, Cambridge (1997)
Augustin, L.M., Luckham, D.C., Gennart, B.A., Huh, Y., Stanculescu, A.G.: Hardware Design and Simulation in VAL/VHDL. Kluwer Academic Pub, Dordrecht (1991)
Brown, S.D., Francis, R.J., Rose, J., Vranesic, Z.G.: Field-Programmable Gate Arrays. Kluwer Academic Publishers, USA (1992)
Cavalcanti, A.L.C., Sampaio, A.C.A., Woodcock, J.C.P.: A refinement strategy for Circus. Formal Aspects Comput. 15(2–3), 146–181 (2003)
Freitas, A., Cavalcanti, A.: 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). https://doi.org/10.1007/11813040_9
Gibson-Robinson, T., Armstrong, P., Boulgakov, A., Roscoe, A.W.: FDR3 — a modern refinement checker for CSP. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 187–201. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-642-54862-8_13
Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Hoboken (1985)
Hinchey, M.G., Jarvis, S.A.: Concurrent Systems: Formal Development in CSP. McGraw-Hill Inc, New York (1995)
Macário, F.J.S., Oliveira, M.V.M.: Hard-wiring CSP hiding: implementing channel abstraction to generate veried concurrent hardware. In: Cornélio, M., Roscoe, B. (eds.) Formal Methods: Foundations and Applications - 18th Brazilian Symposium on Formal Methods. Lecture Notes in Computer Science, vol. 9526, pp. 3–18. The original publication is available at www.springerlink.com, Springer-Verlag (2015)
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, (1994)
Oliveira, M., Cavalcanti, A.: From Circus to JCSP. In: Davies, J., Schulte, W., Barnett, M. (eds.) ICFEM 2004. LNCS, vol. 3308, pp. 320–340. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-30482-1_29
Oliveira, M.V.M., De Medeiros Júnior, I.S., Woodcock, J.: A verified protocol to implement multi-way synchronisation and interleaving in CSP. In: Hierons, R.M., Merayo, M.G., Bravetti, M. (eds.) SEFM 2013. LNCS, vol. 8137, pp. 46–60. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-40561-7_4
Oliveira, M., Woodcock, J.: Automatic generation of verified concurrent hardware. In: Butler, M., Hinchey, M.G., Larrondo-Petrie, M.M. (eds.) ICFEM 2007. LNCS, vol. 4789, pp. 286–306. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-76650-6_17
Phillips, J.D., Stiles,G.S.: An automatic translation of CSP to Handel-C. In: East, I., Martin, J., Welch, P., Duce, D., Green, M., (eds), Communicating Process Architectures 2004, pp. 19–38 (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 (2003)
Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice-Hall Series in Computer Science. Prentice-Hall, Hoboken (1998)
Schneider, S.: Concurrent and Real Time Systems: The CSP Approach, 1st edn. John Wiley, New York (1999)
Sommerville, I.: Software Engineering, 9th edn. Addison-Wesley, Boston (2010)
Stepney, S.: CSP/FDR2 to Handel-C translation. Technical report YCS-2002-357, Department of Computer Science, University of York (2003)
Welch, P.H.: Process oriented design for Java: concurrency for all. In: Arabnia, H.R., editor, Proceedings of the International Conference on Parallel and Distributed Processing Techniques and Applications, pp. 51–57. CSREA Press (2000)
Woodcock, J.C.P., Davies, J.: Using Z-Specification, Refinement, and Proof. Prentice-Hall, Hoboken (1996)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2022 The Author(s), under exclusive license to Springer Nature Switzerland AG
About this paper
Cite this paper
Silva, L., Oliveira, M. (2022). Automatic Generation of Verified Concurrent Hardware Using VHDL. In: Lima, L., Molnár, V. (eds) Formal Methods: Foundations and Applications. SBMF 2022. Lecture Notes in Computer Science, vol 13768. Springer, Cham. https://doi.org/10.1007/978-3-031-22476-8_4
Download citation
DOI: https://doi.org/10.1007/978-3-031-22476-8_4
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-031-22475-1
Online ISBN: 978-3-031-22476-8
eBook Packages: Computer ScienceComputer Science (R0)