This is an open access article published by the IET under the Creative Commons Attribution-NonCommercial-NoDerivs License (http://creativecommons.org/licenses/by-nc-nd/3.0/)
Full text loading...
/deliver/fulltext/iet-cps/4/3/IET-CPS.2018.5008.html;jsessionid=sa7vtwl9ydat.x-iet-live-01?itemId=%2fcontent%2fjournals%2f10.1049%2fiet-cps.2018.5008&mimeType=html&fmt=ahah
References
-
-
1)
-
12. Meijer, S., Nikolov, H., Stefanov, T.: ‘On compile-time evaluation of process partitioning transformations for kahn process networks’. CODES-ISSS'09, Grenoble, France, 2009, pp. 31–40.
-
2)
-
13. Meijer, S., Nikolov, H., Stefanov, T.: ‘Throughput modeling to evaluate process merging transformations in polyhedral process networks’. Proc. of Int. Conf. Design, Automation and Test in Europe (DATE'10), Dresden, Germany, 2010, pp. 747–752.
-
3)
-
45. Jiang, B., Deprettere, E., Kienhuis, B.: ‘Hierarchical run time deadlock detection in process networks’. IEEE Workshop on Signal Processing Systems, Washington DC, USA, 2008, pp. 239–244.
-
4)
-
10. Davare, A., Zhu, Q., Sangiovanni-Vincentelli, A.: ‘A platform-based design flow for kahn process networks’. , UC Berkeley, March 2006.
-
5)
-
28. Holzmann, G.J.: ‘The model checker spin’, IEEE Trans. Softw. Eng., 1997, 23, pp. 279–295.
-
6)
-
48. Oppen, D.C.: ‘A 222pn upper bound on the complexity of presburger arithmetic’, J. Comput. Syst. Sci., 1978, 16, (3), pp. 323–332.
-
7)
-
36. Strehl, K., Thiele, L.: ‘Interval diagrams for efficient symbolic verification of process networks’, IEEE Trans. CAD ICS, 2000, 19, (8), pp. 939–956.
-
8)
-
39. Kienhuis, B., Rijpkema, E., Deprettere, E.F.: ‘Compaan: deriving process networks from matlab for embedded signal processing architectures’. CODES'00, San Diego, CA, USA, 2000, pp. 13–17.
-
9)
-
1. Horowitz, M., Indermaur, T., Gonzalez, R.: ‘Low-power digital design’. IEEE Symp. on Low Power Electronics, San Diego, CA, USA, 1994, pp. 8–11.
-
10)
-
26. Clarke, E.M., Emerson, E.A.: ‘Design and synthesis of synchronization skeletons using branching-time temporal logic’. Logic of Programs, Workshop, Berlin, Heidelberg, 1982, pp. 52–71.
-
11)
-
27. Queille, J.-P., Sifakis, J.: ‘Specification and verification of concurrent systems in cesar’. Proc. of the 5th Colloquium on Int. Symp. on Programming, London, UK, 1982, pp. 337–351.
-
12)
-
24. Park, D.: ‘Concurrency and automata on infinite sequences’. Proc. of the 5th GI-Conf. on Theoretical Computer Science, London, UK, 1981, pp. 167–183.
-
13)
-
9. Nikolov, H., Stefanov, T., Deprettere, E.: ‘Systematic and automated multiprocessor system design, programming, and implementation’, IEEE TCAD ICS, 2008, 27, (3), pp. 542–555.
-
14)
-
17. Karfa, C., Banerjee, K., Sarkar, D., et al: ‘Verification of loop and arithmetic transformations of array-intensive behaviors’, IEEE Trans. CAD ICS, 2013, 32, (11), pp. 1787–1800.
-
15)
-
4. Kahn, G.: ‘The semantics of a simple language for parallel programming’. Proc. of IFIP Congress, Stockholm, Sweden, 1974, pp. 471–475.
-
16)
-
17)
-
3. Turjan, A., Kienhuis, B., Deprettere, E.: ‘Translating affine nested-loop programs to process networks’. CASES'04, Washington DC, USA, 2004, pp. 220–229.
-
18)
-
43. Kelly, W., Rosser, E., Pugh, B., et al: ‘The omega calculator and library’, , 2008. .
-
19)
-
21. Hoare, C.A.R.: ‘Communicating sequential processes’, Commun. ACM, 1978, 21, (8), pp. 666–677.
-
20)
-
29. McMillan, K.L.: ‘Symbolic model checking’ (Kluwer Academic Publishers, Norwell, MA, USA, 1993).
-
21)
-
35. Abadi, M., Lamport, L.: ‘Conjoining specifications’, ACM Trans. Program. Lang. Syst., 1995, 17, (3), pp. 507–535.
-
22)
-
37. Raudvere, T., Sander, I., Jantsch, A.: ‘Application and verification of local nonsemantic-preserving transformations in system design’, IEEE Trans. CAD ICS, 2008, 27, (6), pp. 1091–1103.
-
23)
-
47. Parks, T.M.: ‘Bounded scheduling of process networks’. , EECS Department, University of California, Berkeley, 1995.
-
24)
-
23. Hennessy, M., Milner, R.: ‘On observing nondeterminism and concurrency’. Proc. of the 7th Colloquium on Automata, Languages and Programming, Berlin, Heidelberg, 1980, pp. 299–309.
-
25)
-
19. Kumar, A., Fernando, S., Ha, Y., et al: ‘Multiprocessor systems synthesis for multiple use-cases of multiple applications on fpga’, ACM Trans. Des. Autom. Electron. Syst., 2008, 13, (3), pp. 40:1–40:27.
-
26)
-
27)
-
28)
-
33. Dams, D., Gerth, R., Grumberg, O.: ‘Abstract interpretation of reactive systems’, ACM Trans. Program. Lang. Syst., 1997, 19, (2), pp. 253–291.
-
29)
-
30)
-
22. Bergstra, J., Klop, J.: ‘Process algebra for synchronous communication’, Inf. Control, 1984, 60, (1), pp. 109–137.
-
31)
-
34. Clarke, E.M., Enders, R., Filkorn, T., et al: ‘Exploiting symmetry in temporal logic model checking’, Form. Methods Syst. Des., 1996, 9, (1–2), pp. 77–104.
-
32)
-
46. Olson, A., Evans, B.: ‘Deadlock detection for distributed process networks’. IEEE Int. Conf. on Acoustics, Speech, and Signal Processing, Philadelphia, PA, USA, 2005, , pp. v/73–v/76.
-
33)
-
34)
-
25. Pnueli, A.: ‘The temporal logic of programs’. 18th Annual Symp. on Foundations of Computer Science (sfcs 1977), San Diego, California, USA, October 1977, pp. 46–57.
-
35)
-
15. Kundu, S., Lerner, S., Gupta, R.: ‘Translation validation of high-level synthesis’, IEEE Trans. CAD ICS, 2010, 29, (4), pp. 566–579.
-
36)
-
31. Burch, J.R., Clarke, E.M., Long, D.E., et al: ‘Symbolic model checking for sequential circuit verification’, IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst., 1994, 13, (4), pp. 401–424.
-
37)
-
14. Kundu, S., Tatlock, Z., Lerner, S.: ‘Proving optimizations correct using parameterized program equivalence’. PLDI ‘09, Dublin, Ireland, 2009, pp. 327–337.
-
38)
-
30. Fernandez, J.-C., Garavel, H., Kerbrat, A., et al: ‘Cadp – a protocol validation and verification toolbox’. Proc. of the 8th Int. Conf. on Computer Aided Verification, CAV ‘96, London, UK, 1996, pp. 437–440.
-
39)
-
16. Shashidhar, K.C.: ‘Efficient automatic verification of loop and data-flow transformations by functional equivalence checking’. , Department of Computer Science, Katholieke Universiteit Leuven, Belgium, 2008.
-
40)
-
44. Cheung, E., Chen, X., Hsieh, H., et al: ‘Runtime deadlock analysis for system level design’, Des. Autom. Embedded Syst., 2009, 13, pp. 287–310.
-
41)
-
11. Fei, Y., Ravi, S., Raghunathan, A., et al: ‘Energy-optimizing source code transformations for operating system-driven embedded software’, Trans. Embedded Comput. Syst., 2007, 7, (1), pp. 1–26.
-
42)
-
2. Turjan, A.: ‘Compiling nested loop programs to process networks’. , Leiden University, 2007.
-
43)
-
18. Karfa, C., Sarkar, D., Mandal, C.: ‘Verification of KPN level transformations’. 26th Int. Conf. on VLSI Design, Pune, India, 2013, pp. 338–343.
-
44)
-
38. Chen, X., Hsieh, H., Balarin, F., et al: ‘Formal verification for embedded system designs’, Des. Autom. Embedded Syst., 2003, 8, pp. 139–153.
-
45)
-
40. Manna, Z.: ‘Mathematical theory of computation’ (McGraw-Hill Kogakusha, Tokyo, 1974).
-
46)
-
32. Godefroid, P.: ‘Using partial orders to improve automatic verification methods’. Proc. of the 2Nd Int. Workshop on Computer Aided Verification, CAV ‘90, Berlin, Heidelberg, 1991, pp. 176–185.
-
47)
-
48)
-
20. Milner, R.: ‘A calculus of communicating systems’ (Springer-Verlag, Berlin, Heidelberg, 1982).
http://iet.metastore.ingenta.com/content/journals/10.1049/iet-cps.2018.5008
Related content
content/journals/10.1049/iet-cps.2018.5008
pub_keyword,iet_inspecKeyword,pub_concept
6
6