Part of the book series:Lecture Notes in Computer Science ((LNCS,volume 13768))
Included in the following conference series:
193Accesses
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
Subscribe and save
- Get 10 units per month
- Download Article/Chapter or eBook
- 1 Unit = 1 Article or 1 Chapter
- Cancel anytime
Buy Now
- Chapter
- JPY 3498
- Price includes VAT (Japan)
- eBook
- JPY 6291
- Price includes VAT (Japan)
- Softcover Book
- JPY 7864
- Price includes VAT (Japan)
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 forCircus. Formal Aspects Comput.15(2–3), 146–181 (2003)
Freitas, A., Cavalcanti, A.: Automatic translation fromCircus 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.: FromCircus 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
Universidade Federal do Rio Grande do Norte, Natal, RN, Brazil
Luciano Silva & Marcel Oliveira
- Luciano Silva
You can also search for this author inPubMed Google Scholar
- Marcel Oliveira
You can also search for this author inPubMed Google Scholar
Corresponding author
Correspondence toMarcel Oliveira.
Editor information
Editors and Affiliations
Federal Rural University of Pernambuco, Recife, Brazil
Lucas Lima
Budapest University of Technology and Economics, Budapest, Hungary
Vince Molnár
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
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)
Share this paper
Anyone you share the following link with will be able to read this content:
Sorry, a shareable link is not currently available for this article.
Provided by the Springer Nature SharedIt content-sharing initiative