IJSTR

International Journal of Scientific & Technology Research

Home About Us Scope Editorial Board Blog/Latest News Contact Us
0.2
2019CiteScore
 
10th percentile
Powered by  Scopus
Scopus coverage:
Nov 2018 to May 2020

CALL FOR PAPERS
AUTHORS
DOWNLOADS
CONTACT

IJSTR >> Volume 9 - Issue 8, August 2020 Edition



International Journal of Scientific & Technology Research  
International Journal of Scientific & Technology Research

Website: http://www.ijstr.org

ISSN 2277-8616



Generic Framework For Verifying Embedded Components

[Full Text]

 

AUTHOR(S)

Lamia Eljadiri, Ismail Assayad

 

KEYWORDS

Algorithms, Automation, Embedded Components, Embedded Systems, Formal verification, Framework, LTL Properties, Promela, SystemC, SysVerPml, System design.

 

ABSTRACT

Formal verification has become very useful and popular in last decade in area of embedded systems design and in analysis of critical systems. It can reveal common errors like deadlocks, starvation, check system invariants, but also verify more complex properties defined by LTL formulas whose writing may be very error prone for non expert users. To reduce the time-to-market for embedded systems and assist designers in the complexity of verification step at design time, we advocate the predevelopment of reusable behavioral properties for each family of embedded components to be verified. The proposed approach is to predefine the reusable properties by specifying them as logics on standard input/output signals and standard data values. Obtaining this reusable form enables them to be used for every new component in the product line, hence without the need to spend additional time to redo the verification setup every time a new component is used to create a new design. We have successfully predefined LTL reusable properties for widely used industrial embedded components families such as FIFOs and BUSes, and have performed generic verification using SPIN tool. This paper presents a framework for the formal verification of standard embedded components such us bus protocol, microprocessor, memory blocks, various IP blocks, and a software component. It includes a model checking of embedded systems components. The algorithms are modeled on SystemC and transformed on Promela language (PROcess or PROtocol MEta LAnguage) with the integration of LTL (Linear Temporal Logic) properties extracting from state machines in order to reduce verification complexity. Thus, SysVerPml is not only dedicated to verifying generated properties but also for the automation integration of other properties in models if needed. In the following, we will provide the answer to the problems of component representation on the design system, what properties are appropriate for each component, and how to verify properties. Until now, there have been few research papers directed towards converting SystemC models to Promela language.

 

REFERENCES

[1] H. D. Foster, “Trends in Functional Verification: A (2016) Industry Study”, whitepaper, Mentor Graphics.
[2] Edmund M. Clarke and Jeannette M. Wing. “Formal Methods: State of the Art and Future”. In ACM Computing Survey, volume 28–4, pages 626–643, (December 1996).
[3] Carl-Johan Seger. “An Introduction to Formal Verification”. Technical Report 92–1, Department of Computer Science, University of British Columbia, Canada, (June 1992).
[4] D. D. Gajski, S. Abdi, A. Gerstlauer, and G. Schirner. “Embedded System Design: Modeling, Synthesis and Verification”. Springer, (2009).
[5] E. M. Clarke and E. A. Emerson. “Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic”. In Logic of Programs, Workshop, pages 52–71, London, UK, (1981). Springer-Verlag.
[6] M. J. C. Gordon and T. F. Melham, “Introduction to HOL: A Theorem Proving Environment for Higher Order Logic”, Cambridge University Press, (1993).
[7] Orna Lichtenstein and Amir Pnueli. “Checking that finite state concurrent programs satisfy their linear specification”. In Proceedings of the 12th ACM SIGACT-SIGPLAN POPL’85, pages 97–107, New York, NY, USA, (1985). ACM.
[8] Nina Amla, Robert Kurshan, Kenneth L. McMillan, and Ricardo Medel, “Experimental Analysis of Different Techniques for Bounded Model Checking”, Springer-Verlag Berlin Heidelberg (2003).
[9] T. Gro¨tker, S. Liao, G. Martin, and S. Swan, System Design with SystemC. Kluwer Academic Pub., Hingham, MA, 2002.
[10] G. Holzmann, Spin Model Checker, the: Primer and Reference Manual, 1st ed. Addison-Wesley Professional, 2003.
[11] K. L. McMillan, Symbolic model checking. Kluwer, 1993.
[12] A. Basu, M. Bozga, and J. Sifakis, “Modeling heterogeneous real-time components in bip,” in SEFM ’06. Washington, DC, USA: IEEE Computer Society, 2006, pp. 3–12.
[13] J. Queille and J. Sifakis, “Iterative methods for the analysis of petri nets,” in Application and Theory of Petri Nets, Selected Papers from the First and the Second European Workshop on Application and Theory of Petri Nets, Stasbourg 23.-26. September 1980, Bad Honnef 28.-30. September 1981, 1981, pp. 161–167. [Online]. Available: https://doi.org/10.1007/978-3-642-68353-4 27
[14] O. Lichtenstein and A. Pnueli, “Checking that finite state concurrent programs satisfy their linear specification,” in Proceedings of the 12th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, ser. POPL ’85. New York, NY, USA: ACM, 1985, pp. 97–107. [Online]. Available: http://doi.acm.org/10.1145/318593.318622
[15] E. M. Clarke, Jr., O. Grumberg, and D. A. Peled, Model Checking. Cambridge, MA, USA: MIT Press, 1999.
[16] E. M. Clarke, E. A. Emerson, and A. P. Sistla, “Automatic verification of finite-state concurrent systems using temporal logic specifications,” ACM Trans. Program. Lang. Syst., vol. 8, no. 2, pp. 244–263, 1986. [Online]. Available: http://doi.acm.org/10.1145/5397.5399
[17] Z. Manna and A. Pnueli, The Temporal Logic of Reactive and Concur- rent Systems. New York, NY, USA: Springer-Verlag New York, Inc., 1992.
[18] R. Alur and T. A. Henzinger, Logics and models of real time: A survey. Berlin, Heidelberg: Springer Berlin Heidelberg, 1992, pp. 74–106. [Online]. Available: http://dx.doi.org/10.1007/BFb0031988
[19] S. Almagor, U. Boker, and O. Kupferman, Discounting in LTL. Berlin, Heidelberg: Springer Berlin Heidelberg, 2014, pp. 424–439. [Online].
Available: http://dx.doi.org/10.1007/978-3-642-54862-8 37
[20] A. Ismail, E. J. Lamia, Z. Abdelouahed, and N. Tarik, “The behavior, interaction and priority framework applied to systemc-based embedded systems”, in 13th IEEE/ACS International Conference of Computer Systems and Applications, AICCSA 2016, Agadir, Morocco, (November 29- December 2, 2016).
[21] Ismail Assayad, Lamia Eljadiri, “A platform for systematic verification of embedded components in IP-XACT, SystemC and Promela“, In ICSDE 2018, Rabat, Morocco, (October 18-19, 2018).
[22] Z. Manna and A. Pnueli, Temporal Verification of Reactive Systems: Safety. Springer-Verlag, 1995.
[23] M. Ben-Ari, A. Pnueli, and Z. Manna, “The temporal logic of branching time,” Acta Informatica, vol. 20, no. 3, pp. 207–226, 1983. [Online]. Available: http://dx.doi.org/10.1007/BF01257083
[24] P. Herber, J. Fellmuth, and S. Glesner, “Model checking systemc designs using timed automata,” in Proceedings of the 6th IEEE/ACM/IFIP international conference on Hardware/Software codesign and system synthesis, ser. CODES+ISSS ’08. New York, NY, USA: ACM, 2008, pp. 131–136.
[25] I. Radojevic, Z. Salcic, and P. Roop, “Modelling heterogeneous embed- ded systems: from Esterel and SystemC to DFCharts,” IEEE Design & Test of Computers, vol. 23, no. 5, pp. 348–357, May 2006.
[26] S. Campos, E. Clarke, W. Marrero, and M. Minea, “Verifying the performance of the pci local bus using symbolic techniques,” in Com- puter Design: VLSI in Computers and Processors, 1995. ICCD ’95. Proceedings., 1995 IEEE International Conference on, Oct 1995, pp. 72–78.
[27] D. Groe, H. M. Le, and R. Drechsler, “Proving transaction and system- level properties of untimed systemc tlm designs,” in Eighth ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE 2010), July 2010, pp. 113–122.
[28] “Eclipse Platform Technical Overview”. Technical Report, Object Technology International (OTI) Inc… (2001). http://www.eclipse.org/whitepapers/eclipseoverview.pdf
[29] Holzner Steve, “Eclipse”, O’Reilly, (April 2004).
[30] Holzner Steve, “Eclipse Cookbook”, O’Reilly , (June 2004).
[31] Shavor Sherry, D’Anjou Jim, Fairbrother Scott, Kehn Dan, Kellerman John, McCarthy Pat, “The Java Developer’s Guide to Eclipse”,Addison-Wesley, (2003).
[32] “Managed Build Extensibility Reference Document (for CDT2.1)”, http://www.eclipse.org/cdt/
[33] “Guide for getting started with SystemC development”, by senior consultant Kim Bjerge, Danish technological institute (2007).
[34] Lamia Eljadiri, Ismail Assayad, and Abdelouahed Zakari, “Generic Verification of Safety Properties For SystemC Programs Using Incomplete Interactions”, In ICSDE 2018, Rabat, Morocco, (October 18-19, 2018).
[35] BEN-ARI, Mordechai, “Principles of the Spin Model Checker”. Springer, (2008). – ISBN 978–1–84628–769–5
[36] Robert C. Armstrong, Ratish J. Punnoose, Matthew H. Wong, Jackson R. Mayo, “Survey of Existing Tools for Formal Verification”, Sandia National Laboratories, Albuquerque, New Mexico 87185 and Livermore, California 94550, (December 2014).
[37] Ismail Assayad, Lamia Eljadiri, Abdelouahed Zakari, “Systematic Verification of Embedded Components with Reusable Properties”. In WINCOM 2017, Rabat, Morocco, (November 01-04, 2017).
[38] Lamia Eljadiri, Ismail Assayad, “Generic Framework Architecture for Verifying Embedded Components”, IJACSA journal Volume 11 Issue 6 June 2020.
[39] https://github.com/motib