×

Dynamic and formal verification of embedded systems: A comparative survey. (English) Zbl 1099.68659

Summary: Embedded systems, by their nature, constitute a meeting point for communities with extremely different background. In particular, the high demands for quality and reliability for embedded systems have led to complementary quality assurance efforts: hardware engineers have developed techniques for dynamic verification in terms of co-simulation, which, in particular, addresses the different nature of hardware and software components. Thus these techniques are tailored for the transactional level, which comprises dedicated models for the hardware and the software parts. On the other hand, there is a bulk of work on formal verification techniques, which typically address higher levels of abstraction. These techniques are exhaustive in the sense that they cover all the infinite possible paths of their models, however at the price of neglecting many of the low-level aspects treated by co-simulation. It is the goal of this paper to increase the mutual understanding between these communities and to animate research at this exciting borderline.

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
PDFBibTeX XMLCite
Full Text: DOI

References:

[3] R. A. Bergamaschi and J. Cohn, The A to Z of SoCs, IEEE, pp. 791–798 (2002)
[4] S. M. Sze, Physics of Semiconductor Devices, John Wiley and Sons (1981)
[5] S. Hall, G. Hall, and J. McCall, High-Speed Digital System Design: A Handbook of Interconnect Theory and Design Practices, John Wiley and Sons (2000)
[6] L. Benini and M. Poncino, Ambient Intelligence: A Computational Platform Perspective, Ambient Intelligence: Impact on Embedded System Design, Kluwer Academic Publishers, pp. 31–50 (2003)
[10] E. Clarke, O. Grumberg, and D. Peled, Model Checking, MIT Press (2000)
[11] L. Cortes, P. Eles, and Z. Peng, Hierarchical Modeling and Verification of Embedded Systems, Proceedings of IEEE Euromicro Symposium on Digital System Design, pp. 63–70 (2001)
[12] L. Gomes and J. P. Barros, On Structuring Mechanisms for Petri Nets based Systems Design, IEEE, pp. 431–438 (2003)
[13] R. Ernst and A. A. Jerraya, Embedded System Design with Multiple Languages, Proceedings of IEEE Conference on Asia and South Pacific Design Automation, pp. 391–396 (2000)
[14] Synopsys Inc., SystemC User’s Guide, http://www.systemc.org
[15] J. Armstrong and F. Gray, VHDL Design Representation and Synthesis, Prentice Hall (2000)
[16] V. Sagdeo, The Complete Verilog Book, Kluwer Academic Publisher (1998) · Zbl 0914.68028
[17] M. Breuer, M. Abramovici, and A. Friedman, Digital Systems Testing and Testable Design, IEEE Press (1990)
[18] D. Gajski, N. Dutt, S. Allen, C. Wu, and Y. Lin, High-Level Synthesis: Introduction to Chip and System Design, 1st edn., Kluwer Academic Publishers (1992)
[19] J. Bergeron, Writing Testbenches: Functional Verification of HDL Models, Kluwer Academic Publishers, Norwell Massachusetts (2000) · Zbl 0944.68187
[22] F. Balarin, M. Chiodo, P. Giusto, H. Hsieh, A. Jurecska, L Lavagno, C. Passerone, A. Sangiovanni-Vincentelli, E. Sentovich, K. Suzuki, and B. Tabbara, Hardware-Software Co-Design of Embedded Systems: The Polis Approach, Kluwer Academic Press (1997) · Zbl 0878.68133
[23] Synopsys Inc., Eaglei, http://www.synopsys.com/products
[24] Mentor Graphics Inc., Seamless CVE, http://www.mentor.com/seamless
[27] P. Coste, F. Hessel, P. L. Marrec, Z. Sugar, M. Romdhani, R Suescun, N. Zergainoh, and A. Jerraya, Multilanguage Design of Heterogeneous Systems, Proceedings of IEEE International Workshop on Hardware-Software Codesign, pp. 54–58 (1999) · Zbl 0968.68528
[29] J. Liu, M. Lajolo, and A. Sangiovanni-Vincentelli, Software Timing Analysis Using HW/SW Co-Simulation and Instruction Set Simulator, Proceedings of IEEE International Workshop on Hardware/Software Co-design, pp. 65–69 (1998)
[30] L. Semeria and A. Ghosh, Methodology for Hardware/Software Co-verification in C/C++, Proceedings of IEEE Asian and South Pacific Design Automation Conference (ASP-DAC), pp 405–408 (2000)
[31] K. Lahiri, A. Raghunathan, G. Lakshminarayana, and S. Dey, Communication Architecture Tuners: A Methodology for the Design of High-Performance Communication Architectures for System-on-Chips, Proceedings of ACM/IEEE Design Automation Conference (DAC), pp. 513–518 (2000)
[32] F. Fummi, S. Martini, G. Perbellini, and M. Poncino, Native ISS-SystemC Integration for the Co-simulation of Multi-Processors SoC, Proceedings of IEEE Design Automation and Test in Europe, pp. 564–569 (2004)
[33] I. Moussa, T. Grellier, and G. Nguyen, Exploring SW Performance Using SoC Transaction-level Modelling, Proceedings of IEEE Design Automation and Test in Europe, pp. 120–125 (2003)
[34] GNU Project Web server, http://www.gnu.org/software/
[35] S. Yoo, I. Bacivarov, A. Bouchhima, Y. Paviot, and A. Jerraya, Building Fast and Accurate SW Simulation Models Based on Hardware Abstraction Layer and Simulation Environment Abstraction Layer, Proceedings of IEEE Design Automation and Test in Europe, pp 550–555 (2003)
[36] I. Bacivarov, S. Yoo, and A. Jerraya, Timed HW-SW Cosimulation Using Native Execution of OS and Application SW, Proceedings of IEEE International High Level Design Validation and Test Workshop, pp. 51–56 (2002)
[37] L. Formaggio, F. Fummi, and G. Pravadelli, A Timing-Accurate HW/SW Co-simulation of an ISS with SystemC, Proceedings of IEEE International Conference on Hardware/Software Codesign and System Synthesis, pp. 152–157 (2004)
[38] ITUTS. ITUTS Recommendation Z.100: Specification and Description Language (SDL) (1988)
[39] ITUTS. ITUTS Recommendation Z.120: Message Sequence Chart (MSC) (1994)
[40] ITUTS. ITUTS Recommendation Z.120 Annex B: Algebraic semantics of Message Sequence Charts (1995)
[42] E. Clarke, O. Grumberg, H. Hiraishi, D. L. S. Jha, K. McMillan, and L. Ness, Verfication of the Futurebus+Cache Coherence Protocol, Proceedings of International Symposium on Computer Hardware Description Languages and their Applications (1993)
[45] J. -P. Katoen, H. Bohnenkamp, H. Hermanns, and J. Klaren, Embedded Software Analysis with MOTOR, Formal Methods for the Design of Computer, Communication and Software Systems: Real Time (2004) · Zbl 1105.68335
[46] R. Milner, Communication and Concurrency, Prentice Hall (1989)
[47] C. Hoare, Communicating Sequential Processes, Prentice Hall (1986) · Zbl 0569.68019
[48] C. Tofts, A Synchronous Calculus of Relative Frequency, CONCUR, LNCS, Vol. 458, pp. 467–480 (1990)
[49] ISO Standard 8807: LOTOS – A Formal Description Technique based on the Temporal Ordering of Observational Behaviour (1989)
[50] S. Förster, A. Windisch, M. Fischer, D. Monjau, and B. Balser, Process Algebraic Specification, Refinement, and Verification of Embedded Systems, Proceedings of ECSI Forum on Specification and Design Languages, pp. 525–535 (2003)
[52] N. Halbwachs, Synchronous Programming of Reactive Systems, Kluwer Academic Publisher (1993) · Zbl 0828.68038
[53] D. Harel, Statecharts: A Visual Formalism for Complex Systems, Science of Computing Programming, pp. 231–274 (1987) · Zbl 0637.68010
[54] F. Maraninchi, Argonaute: Graphical Description, Semantics and Verification of Reactive Systems by using a Process Algebra, Proceedings of Int. Workshop on Automatic Verification Methods for Finite State Systems, pp. 38–53 (1990)
[55] C. Andrè, SyncCharts: A Visual Representation of Reactive Behaviors, Technical Report TR-92-52, Universitè de Nice, Sophia-Antipolis (1995)
[56] W. Damm and D. Harel, LSC: Breathing Life into Message Sequence Charts, Formal Methods in System Design, pp. 45–80 (2001) · Zbl 0985.68033
[57] N. Halbwachs, P. Caspi, and D. Pilaud, The Synchronous Programming Language Lustre, Proceedings of IEEE, pp. 1305–1320 (1991)
[59] Esterel Technologies: The SCADE Suite for Safety-Critical Software Development, http://www.esterel-technologies.com/v2/scadeSuiteForSafetyCriticalSoftwareDevelopment
[60] G. Berry, The Foundations of Esterel, MIT Press (1988)
[61] G. Berry, The Constructive Semantics of Pure Esterel, http://www.esterel-technologies.com
[63] C. Dumoulin, J. -L. Dekeyser, B. Kokoszko, S. Pulon, and G Cristau, Interoperability between Design and Simulation Tools using Model Transformation Techniques, Proceedings of ECSI Forum on Specification and Design Languages (2003)
[64] W. Müller and G. Martin, DAC 2004 Workshop on UML for SoC Design, Proceedings of Workshop on Specification and Validation of UML Models for Real-Time Embedded Systems (2004)
[65] W. Tan, P. Thiagarajan, W. Wong, Y. Zhu, and S. Pilakkat, Synthesizable SystemC Code from UML Models, DAC Workshop on UML for SoC Design (2004)
[66] P. Boulet, A. Cuccuru, J.-L. Dekeyser, C. Dumoulin, P. Marquet, M. Samyn, R. D. Simone, G. Siegel, and T. Saunier, MDA for SoC Design: UML To SystemC Experiment, DAC Workshop on UML for SoC Design (2004)
[67] The Omega Project, http://www-omega.imag.fr
[68] M. Bozga, J. Fernandez, L. Ghirvu, S. Graf, J. Krimm, and L Mounier, An Intermediate Representation and Validation Environment for Timed Asynchronous Systems, Formal Methods’99, LNCS, Vol. 1708, pp. 307–327 (1999) · Zbl 0974.68556
[69] I. Ober, S. Graf, and I. Ober, Model Checking of UML Models via a Mapping to Communicating Extended Timed Automata, SPIN Workshop on Model Checking of Software (2004) · Zbl 1125.68371
[70] S. Graf and J. Hooman, Correct Development of Embedded Systems, Proceedings of European Workshop of Software Architecture (2004)
[71] M. Bozga, S. Graf, and L. Mounier, IF-2.0: A Validation Environment for Component-based Real-Time Systems, Proceedings of International Conference on computer Aided Verification, LNCS, Vol. 2404, pp. 343–348 (2002) · Zbl 1010.68751
[72] M. Bozga, S. Graf, and L. Mounier, Automated Validation of Distributed Software Using the IF Environment, Proceedings of IEEE International Symposium on Network Computing and Applications, pp. 268–275 (2001)
[73] D. Harel, H. Kugler, R. Marelly, and A. Pnueli, Smart Play-out, Proceedings of ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (2003)
[74] T. Bienmller, W. Damm, and H. Wittke, The STATEMATE Verification Environment Making it Real, Proceedings of International Conference on computer Aided Verification, LNCS, Vol. 1855, pp. 561–567 (2000) · Zbl 0974.68564
[75] N. Shankar, S. Owre, and J. Rushby, The PVS Proof Checker: A Reference Manual, Technical report, Computer Science Laboratory, SRI International (1993)
[76] M. Kyas and F. de Boer, On message specification in OCL, Compositional Verification in UML, Workshop associated with UML 2003 (2003)
[77] M. Zwaag and J. Hooman, A Semantics of Communicating Reactive Objects with Timing, Proceedings of Workshop on Specification and Validation of UML models for Real-Time Embedded Systems (2003)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.