Abstract
In the context of specification of complex digital systems and their implementation on FPGA, a tool-based methodology is developed using a component-based approach. The component’s behavior is described by means of Interpreted Prioritized Time Petri nets which are formalized in this article. Formal analysis is used to validate the model’s properties and to optimize its implementation. Our approach is illustrated on the micro machine of a distributed stimulation unit.
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
Kralj, A., Bajd, T.: Functional Electrical Stimulation: Standing and Walking After Spinal Cord Injury. Chemical Rubber Company (CRC Press), Boca Raton (1989)
Rodriguez-Andina, J.J., Moure, M.J., Valdes, M.D.: Features, Design Tools, and Application Domains of FPGAs. IEEE Transactions on Industrial Electronics 54(4) (August 2007)
Navabi, Z.: VHDL: Analysis and Modeling of Digital Systems. McGraw-Hill (1997)
Souquet, G., Andreu, D., Guiraud, D.: Petri nets based methodology for communicating neuroprothesis design and prototyping. In: ISABEL, Aalborg, Denmark (2008)
Andreu, D., Souquet, G., Gil, T.: Petri Net Based Rapid Prototyping of Digital Complex System. In: ISVLSI, Montpellier, France (2008)
David, R., Alla, H.: Discrete, Continuous, and Hybrid Petri nets. Springer (2005)
Murata, T.: Petri nets: Properties, analysis and applications. Proceedings of the IEEE 77(4), 541–580 (1989)
Berthomieu, B., Peres, F., Vernadat, F.: Model Checking Bounded Prioritized Time Petri Nets. In: Namjoshi, K.S., Yoneda, T., Higashino, T., Okamura, Y. (eds.) ATVA 2007. LNCS, vol. 4762, pp. 523–532. Springer, Heidelberg (2007)
Berthomieu, B., Ribet, P.O., Vernadat, F.: The tool TINA – Construction of Abstract State Spaces for Petri Nets and Time Petri Nets. International Journal of Production Research 42(14) (2004)
Traonouez, L.M., Lime, D., Roux, O.: Parametric Model-Checking of Stopwatch Petri Nets. Journal of Universal Computer Science 15(17), 3273–3304 (2009)
Royal, A., Cheung, P.Y.K.: Globally asynchronous locally synchronous FPGA architectures. In: Cheung, P.Y.K., Constantinides, G.A. (eds.) FPL 2003. LNCS, vol. 2778, pp. 355–364. Springer, Heidelberg (2003)
Billington, J., et al.: The Petri Net Markup Language: Concepts, Technology, and Tools. In: van der Aalst, W.M.P., Best, E. (eds.) ICATPN 2003. LNCS, vol. 2679, pp. 483–505. Springer, Heidelberg (2003)
Godary-Dejean, K., Andreu, D.: Formal Validation of a Deterministic MAC Protocol. ACM Trans. Embed. Comput. Syst., 6:1–6:23 (2013)
Andreu, D., Guiraud, D., Souquet, G.: A Distributed Architecture for Activating the Peripheral Nervous System. Jounal of Neural Engineering 6, 1–18 (2009)
Petri, C.A.: Kommunikation mit Automaten. Dissertation der Fakultät für Mathematik und Physik, Technische Hochschule Darmstadt, Bonn (1962)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Leroux, H., Godary-Dejean, K., Andreu, D. (2013). Complex Digital System Design: A Methodology and Its Application to Medical Implants. In: Pecheur, C., Dierkes, M. (eds) Formal Methods for Industrial Critical Systems. FMICS 2013. Lecture Notes in Computer Science, vol 8187. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-41010-9_7
Download citation
DOI: https://doi.org/10.1007/978-3-642-41010-9_7
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-41009-3
Online ISBN: 978-3-642-41010-9
eBook Packages: Computer ScienceComputer Science (R0)