[1] Accellera Systems Initiative. (2011). IEEE 1666 Standard: SystemC Language Reference Manual. Retrieved from http://www.accellera.org
[2] Blanc, Nicolas., Kroening, Daniel. (2008). Race analysis for SystemC using model checking. In 2008 International Conference on Computer-Aided Design (ICCAD’08) (pp. 356–363). IEEE. doi:10.1145/1509456.1509540
[3] Cimatti, Alessandro, Narasamdya, Iman., Roveri, Marco. (2013). Software model checking SystemC. IEEE Transactions on CAD of Integrated Circuits and Systems, 32(5), 774–787. doi:10.1109/TCAD.2012.2232351
[4] Drechsler, Rolf., Große, Daniel. (2002). Reachability analysis for formal verification of SystemC. In 2002 Euromicro Symposium on Digital Systems Design (DSD 2002), Systems-on-Chip (pp. 337–340). IEEE Computer Society. doi:10.1109/DSD.2002.1115387
[5] Flanagan, Cormac., Godefroid, Patrice. (2005). Dynamic partial-order reduction for model checking software. In Proceedings of the 32nd ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, POPL 2005 (pp. 110–121). ACM. doi:10.1145/1040305.1040315
[6] Garavel, Hubert. (1998). Open/cæsar: An OPen software architecture for verification, simulation, and testing. In Tools and Algorithms for Construction and Analysis of Systems, 4th International Conference, TACAS ’98, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS’98, Lisbon, Portugal, March 28 – April 4, 1998, Proceedings (pp. 68–84). Springer. doi:10.1007/BFb0054165
[7] Garavel, Hubert, Helmstetter, Claude, Ponsini, Olivier., Serwe, Wendelin. (2009). Verification of an industrial SystemC/TLM model using LOTOS and CADP. In 7th ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE 2009) (pp. 46–55). IEEE Computer Society. doi:10.1109/MEMCOD.2009.5185377
[8] Garavel, Hubert, Lang, Frédéric., Mateescu, Radu. (2002). An overview of CADP 2001. European Association for Software Science and Technology (EASST) Newsletter, 4, 13–24.
[9] Garavel, Hubert, Mateescu, Radu, Lang, Frédéric., Serwe, Wendelin. (2007). CADP 2006: A toolbox for the construction and analysis of distributed processes. In Computer Aided Verification, 19th International Conference, CAV 2007, Berlin, Germany, July 3–7, 2007, Proceedings (Vol. 4590, pp. 158–163). Springer. doi:10.1007/978-3-540-73368-3_18
[10] Ghenassia, Frank (Ed.). (2005). Transaction-Level Modeling with SystemC. TLM Concepts and Applications for Embedded Systems. Springer. ISBN 0-387-26232-6.
[11] Große, Daniel., Drechsler, Rolf. (2005). CheckSyC: an efficient property checker for RTL SystemC designs. In International Symposium on Circuits and Systems (ISCAS 2005) (Vol. 4, pp. 4167–4170). IEEE. doi:10.1109/ISCAS.2005.1465549
[12] Große, Daniel, Le, Hoang M.., Drechsler, Rolf. (2010). Proving transaction and systemlevel properties of untimed SystemC TLM designs. In 8th ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE 2010) (pp. 113–122). IEEE Computer Society. doi:10.1109/MEMCOD.2010.5558643
[13] Helmstetter, Claude. (2007). Validation de modèles de systems sur puce enprésenced’ or donnancementsindéterministes et de temps imprécis. PhD thesis, INPG, Grenoble, France. Retrieved from http://tel.archives-ouvertes.fr/tel-00350929
[14] Helmstetter, Claude, Maraninchi, Florence., Maillet-Contoz, Laurent. (2006). Test coverage for loose timing annotations. In Formal Methods: Applications and Technology, 11th International Workshop, FMICS 2006 and 5th International Workshop PDMC 2006, Bonn, Germany, August 26– 27, and August 31, 2006, Revised Selected Papers (Vol. 4346, pp. 100–115). Springer. doi:10.1007/978-3-540-70952-7_7
[15] Helmstetter, Claude, Maraninchi, Florence., Maillet-Contoz, Laurent. (2009). Full simulation coverage for SystemC transaction-level models of systems-on-a-chip. Formal Methods in System Design, 35(2), 152–189. doi:10.1007/s10703-009-0075-z
[16] Helmstetter, Claude., Ponsini, Olivier. (2008). A comparison of two SystemC/TLM semantics for formal verification. In 6th ACM & IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE 2008) (pp. 59–68). IEEE Computer Society. doi:10.1109/ MEMCOD.2008.4547687
[17] Herber, Paula, Pockrandt, Marcel., Glesner, Sabine. (2011). Transforming SystemC transaction level models into UPPAAL timed automata. In 9th IEEE/ACM International Conference on Formal Methods and Models for Codesign, MEMOCODE 2011, Cambridge, UK, 11–13 July, 2011 (pp. 161–170). IEEE. doi:10.1109/MEMCOD.2011.5970523
[18] ISO/IEC. (1989). Lotos – a formal description technique based on the temporal ordering of observational behaviour. International Standard 8807. International Organization for Standardization – Information Processing Systems – Open Systems Interconnection, Genève.
[19] Joloboff, Vania., Helmstetter, Claude. (2008). SimSoC: A SystemC TLM integrated ISS for full system simulation. In Circuits and Systems, 2008. APCCAS 2008. IEEE Asia Pacific Conference on. IEEE. doi:10.1109/APCCAS.2008.4746381
[20] Kroening, Daniel., Sharygina, Natasha. (2005). Formal verification of SystemC by automatic hardware/software partitioning. In 3rd ACM & IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE 2005), 11–14 July 2005, Verona, Italy, Proceedings (pp. 101–110). IEEE. doi:10.1109/MEMCOD.2005.1487900
[21] Kundu, Sudipta, Ganai, Malay K.., Gupta, Rajesh. (2008). Partial order reduction for scalable testing of SystemC TLM designs. In Proceedings of the 45th Design Automation Conference, DAC 2008, Anaheim, CA, USA, June 8–13, 2008 (pp. 936–941). ACM. doi:10.1145/1391469.1391706
[22] Marquet, Kevin, Moy, Matthieu., Jeannet, Bertrand. (2011). Efficient Encoding of SystemC/ TLM in Promela. In Workshop on Design, Analysis and Tools for Integrated Circuits and Systems at the International MultiConference of Engineers and Computer Scientists 2011, DATICS-IMECS (pp. 1039–1044). Retrieved from http://www.iaeng.org/publication/IMECS2011/ IMECS2011_pp1039-1044.pdf
[23] Moy, Matthieu. (2005). Techniques and Tools for the Verification of Systems-on-a-Chip at the Transaction Level. PhD thesis, INPG, Grenoble, France. Retrieved from http://wwwverimag.imag.fr/~moy/phd/
[24] Moy, Matthieu, Maraninchi, Florence., Maillet-Contoz, Laurent. (2005). LusSy: an open tool for the analysis of systems-on-a-chip at the transaction level. Design Automation for Embedded Systems, 10(2–3), 73–104. doi:10.1007/s10617-006-9044-6
[25] Niemann, Bernhard., Haubelt, Christian. (2006). Formalizing TLM with communicating state machines. In Forum on specification and Design Languages, FDL 2006, September 19–22, 2006, Darmstadt, Germany, Proceedings (pp. 285–293). ECSI.
[26] Ponsini, Olivier., Serwe, Wendelin. (2008). A schedulerless semantics of TLM models written in SystemC via translation into LOTOS. In FM 2008: Formal Methods, 15th International Symposium on Formal Methods, Turku, Finland, May 26–30, 2008, Proceedings (Vol. 5014, pp. 278–293). Springer. doi:10.1007/978-3-540-68237-0_20
[27] Traulsen, Claus, Cornet, Jérôme, Moy, Matthieu., Maraninchi, Florence. (2007). A SystemC/ TLM semantics in Promela and its possible applications. In Model Checking Software, 14th International SPIN Workshop, Berlin, Germany, July 1–3, 2007, Proceedings (Vol. 4595, pp. 204– 222). Springer. doi:10.1007/978-3-540-73370-6_14