The Community for Technology Leaders
RSS Icon
Issue No.10 - Oct. (2013 vol.62)
pp: 1917-1931
Soumyajit Dey , Indian Institute of Technology, Patna
Dipankar Sarkar , Indian Institute of Technology, Kharagpur
Anupam Basu , Indian Institute of Technology, Kharagpur
The tagged signal model (TSM) is a formal framework for modeling heterogeneous embedded systems. In the present work, we provide a representation of tagged systems using the semantics of Kleene algebra. We further illustrate mechanisms for both behavioral transformational verification through equivalence checking and property verification of heterogeneous embedded systems based on this algebraic representation.
Algebra, Computational modeling, Acceleration, Embedded systems, Upper bound, Protocols, Mathematical model, Kleene algebra, Tagged signal model, heterogeneous embedded systems, actor theory
Soumyajit Dey, Dipankar Sarkar, Anupam Basu, "A Kleene Algebra of Tagged System Actors for Reasoning about Heterogeneous Embedded Systems", IEEE Transactions on Computers, vol.62, no. 10, pp. 1917-1931, Oct. 2013, doi:10.1109/TC.2012.134
[1] L. Lavagno, A. Sangiovanni-vincentelli, and E. Sentovich, "Models of Computation for Embedded System Design," Proc. NATO ASI System Synthesis, pp. 45-102, 1998.
[2] A. Jantsch and I. Sander, "Models of Computation and Languages for Embedded System Design," IEE Proc., vol. 152, no. 2, pp. 114-129, Mar. 2005.
[3] J. Eker, J.W. Janneck, E.A. Lee, J. Liu, X. Liu, J. Ludvig, S. Neuendorffer, S. Sachs, and Y. Xiong, "Taming Heterogeneity - The Ptolemy Approach," Proc. IEEE, vol. 91, no. 1, pp. 127-144, Jan. 2003.
[4] E.A. Lee and Y. Xiong, "System-Level Types for Component-Based Design," Proc. First Int'l Workshop Embedded Software (EMSOFT), pp. 237-253, 2001.
[5] R. Alur, T. Dang, J. Esposito, Y. Hur, F. Ivancic, R.V. Kumar, I. Lee, P. Mishra, G.J. Pappas, and O. Sokolsky, "Hierarchical Modeling and Analysis of Embedded Systems," Proc. IEEE, vol. 91, no. 1, pp. 11-28, Jan. 2003.
[6] F. Balarin, Y. Watanabe, H. Hsieh, L. Lavagno, C. Passerone, and A. Sangiovanni-Vincentelli, "Metropolis: An Integrated Electronic System Design Environment," Computer, vol. 36, no. 4, pp. 45-52, Apr. 2003.
[7] J. Burch, "Overcoming Heterophobia: Modeling Concurrency in Heterogeneous Systems," Proc. Int'l Conf. Application of Concurrency to System Design (ACSD), pp. 13-32, 2001.
[8] I. Sander and A. Jantsch, "System Modeling and Design Refinement in ForSyDe," IEEE Trans. Computer-Aided Design of Integrated Circuits and Systems, vol. 23, no. 1, pp. 17-32, Jan. 2004.
[9] D.A. Mathaikutty, H.D. Patel, S.K. Shukla, and A. Jantsch, "SML-Sys: A Functional Framework with Multiple Models of Computation for Modeling Heterogeneous System," Design Automation for Embedded Systems, vol. 12, nos. 1/2, pp. 1-30, June 2008.
[10] E. Lee and A. Sangiovanni-Vincentelli, "A Framework for Comparing Models of Computation," IEEE Trans. Computer-Aided Design of Integrated Circuits and Systems, vol. 17, no. 12, pp. 1217-1229, Dec. 1998.
[11] A. Benveniste, B. Caillaud, L.P. Carloni, P. Caspi, and A.L. Sangiovanni-Vincentelli, "Composing Heterogeneous Reactive Systems," ACM Trans. Embedded Computing Systems, vol. 7, no. 4, pp. 43:1-43:36, Aug. 2008.
[12] G. Agha and C. Hewitt, "Concurrent Programming Using Actors," Object-Oriented Concurrent Programming, pp. 37-53, MIT Press, 1987.
[13] D. Kozen, "Kleene Algebra with Tests," ACM Trans. Programming Language and Systems, vol. 19, no. 3, pp. 427-443, May 1997.
[14] H. Kopetz and G. Bauer, "The Time-Triggered Architecture," Proc. IEEE, vol. 91, no. 1, pp. 112-126, Jan. 2003.
[15] A. Benveniste, B. Caillaud, L.P. Carloni, and A.L. Sangiovanni-Vincentelli, "Tag Machines," Proc. Fifth ACM Int'l Conf. Embedded Software (EMSOFT), pp. 255-263, 2005.
[16] X. Liu and E.A. Lee, "CPO Semantics of Timed Interactive Actor Networks," Theoretical Computer Science, vol. 409, no. 1, pp. 110-125, 2008.
[17] W. Clinger, "Foundations of Actor Semantics," PhD dissertation, MIT, 1981.
[18] G.D. Plotkin, "A Powerdomain Construction," SIAM J. Computing, vol. 5, no. 3, pp. 452-487, 1976.
[19] A. Platzer and J.-D. Quesel, "European Train Control System: A Case Study in Formal Verification," Proc. Int'l Conf. Formal Eng. Methods (ICFEM), pp. 246-265, 2009.
[20] S. Dey, D. Sarkar, and A. Basu, "A Kleene Algebra of Tagged System Actors," IEEE Embedded Systems Letters, vol. 3, no. 1, pp. 28-31, Mar. 2011.
[21] W. Damm, A. Mikschl, J. Oehlerking, E. Olderog, J. Pang, A. Platzer, M. Segelken, and B. Wirtz, "Automating Verification of Cooperation, Control and Design in Traffic Applications," Formal Methods and Hybrid Real-Time Systems, C.B. Jones, Z. Liu, and J. Woodcock, eds., pp. 115-169, Springer-Verlag, 2007.
[22] B.A. Davey and H.A. Priestley, Introduction to Lattices and Order. Cambridge Univ. Press, Apr. 2002.
[23] P. Caspi, A. Benveniste, R. Lublinerman, and S. Tripakis, "Actors without Directors: A Kahnian View of Heterogeneous Systems," Proc. 12th Int'l Conf. Hybrid Systems: Computation and Control (HSCC '09), pp. 46-60, 2009.
[24] P. Knijnenburg, "Algebraic Domains, Chain Completion and the Plotkin Powerdomain Construction," technical report, Dept. of Computer Science, Univ. of Utrecht, 1993.
[25] Z. Manna and A. Pnueli, "Axiomatic Approach to Total Correctness of Programs," Acta Informatica, vol. 3, pp. 243-263, 1974.
[26] B. Möller and G. Struth, "Modal Kleene Algebra and Partial Correctness," Proc. Int'l Conf. Algebraic Methodology and Software Technology (AMAST), pp. 379-393, 2004.
[27] D. Kozen, "On Hoare Logic and Kleene Algebra with Tests," ACM Trans. Computational Logic, vol. 1, no. 1, pp. 60-76, 2000.
[28] P. Höfner and G. Struth, "Automated Reasoning in Kleene Algebra," Proc. 21st Int'l Conf. Automated Deduction (CADE-21), pp. 279-294, 2007.
[29] K. Aboul-Hosn and D. Kozen, "KAT-ML: An Interactive Theorem Prover for Kleene Algebra with Tests," J. Applied Non-Classical Logics, vol. 16, nos. 1/2, pp. 9-34, 2003.
[30] D. Kozen, "Nonlocal Flow of Control and Kleene Algebra with Tests," Proc. Symp. Logic in Computer Science, pp. 105-117, 2008.
41 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool