Abstract
Systems that can immediately react to their inputs may suffer from cyclic dependencies between their actions and the corresponding trigger conditions. For this reason, causality analysis has to be employed to check the constructiveness of the programs which implies the existence of unique and consistent behaviours. In this paper, we describe the embedding of various views of causality analysis into the HOL4 theorem prover to check their equivalence. In particular, we show the equivalence between the classical analysis procedure, which is based on a fixpoint computation, and a formulation as a (bounded) model checking problem.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Andersen, F.: A Theorem Prover for UNITY in Higher Order Logic. PhD thesis, Horsholm, Denmark (March 1992)
Andersen, F., Petersen, K.D., Petterson, J.S.: Program verification using HOL-UNITY. In: Joyce, J.J., Seger, C.-J.H. (eds.) HUG 1993. LNCS, vol. 780, pp. 1–15. Springer, Heidelberg (1994)
Benveniste, A., Caspi, P., Edwards, S., Halbwachs, N., Le Guernic, P., de Simone, R.: The synchronous languages twelve years later. Proceedings of the IEEE 91(1), 64–83 (2003)
Berry, G.: The constructive semantics of pure Esterel (July 1999), http://www-sop.inria.fr/esterel.org/
Brzozowski, J.A., Seger, C.-J.: Asynchronous Circuits. Springer, Heidelberg (1995)
Chandy, K.M., Misra, J.: Parallel Program Design, May 1989. Addison Wesley, Austin, Texas (1989)
Collins, G., Syme, D.: A theory of finite maps. In: Schubert, E.T., Alves-Foss, J., Windley, P. (eds.) HUG 1995. LNCS, vol. 971, pp. 122–137. Springer, Heidelberg (1995)
Girault, A., Lee, B., Lee, E.: Hierarchical finite state machines with multiple concurrency models. IEEE Transactions on Computer Aided Design of Integrated Circuits and Systems 18(6), 742–760 (1999)
Huffman, D.: Combinational circuits with feedback. In: Mukhopadhyay, A. (ed.) Recent Developments in Switching Theory, pp. 27–55. Academic Press, London (1971)
Jantsch, A.: Modeling Embedded Systems and SoCs. Morgan Kaufmann, San Francisco (2004)
Kautz, W.: The necessity of closed circuit loops in minimal combinational circuits. IEEE Transactions on Computers C-19(2), 162–166 (1970)
Lee, E., Sangiovanni-Vincentelli, A.: A framework for comparing models of computation. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 17(12), 1217–1229 (1998)
Malik, S.: Analysis of cycle combinational circuits. IEEE Transactions on Computer Aided Design 13(7), 950–956 (1994)
Riedel, M.: Cyclic Combinational Circuits. PhD thesis, California Institute of Technology, Passadena, California (2004)
Riedel, M.D., Bruck, J.: Cyclic combinational circuits: Analysis for synthesis. In: International Workshop on Logic and Synthesis (IWLS), Laguna Beach, California (2003)
Riedel, M.D., Bruck, J.: The synthesis of cyclic combinational circuits. In: Design Automation Conference (DAC), Anaheim, California, USA, pp. 163–168. ACM Press, New York (2003)
Rivest, R.: The necessity of feedback in minimal monotone combinational circuits. IEEE Transactions on Computers C-26(6), 606–607 (1977)
Schneider, K.: The synchronous programming language Quartz. Internal Report, Department of Computer Science, University of Kaiserslautern (to appear, 2008)
Schneider, K., Brandt, J., Schuele, T.: Causality analysis of synchronous programs with delayed actions. In: Compilers, Architecture, and Synthesis for Embedded Systems (CASES), pp. 179–189. ACM Press, New York (2004)
Schneider, K., Brandt, J., Schuele, T., Tuerk, T.: Improving constructiveness in code generators. In: Synchronous Languages, Applications, and Programming (SLAP), Edinburgh, United Kingdom (2005)
Schneider, K., Brandt, J., Schuele, T., Tuerk, T.: Maximal causality analysis. In: Application of Concurrency to System Design (ACSD), St. Malo, France, pp. 106–115. IEEE Computer Society, Los Alamitos (2005)
Shiple, T.R., Berry, G., Touati, H.: Constructive analysis of cyclic circuits. In: European Design and Test Conference (EDTC), Paris, France. IEEE Computer Society Press, Los Alamitos (1996)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Brandt, J., Schneider, K. (2008). Formal Reasoning About Causality Analysis. In: Mohamed, O.A., Muñoz, C., Tahar, S. (eds) Theorem Proving in Higher Order Logics. TPHOLs 2008. Lecture Notes in Computer Science, vol 5170. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-71067-7_13
Download citation
DOI: https://doi.org/10.1007/978-3-540-71067-7_13
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-71065-3
Online ISBN: 978-3-540-71067-7
eBook Packages: Computer ScienceComputer Science (R0)