Technical systems in logic: questions of formalization and automatic verification
##plugins.themes.bootstrap3.article.sidebar##
Published:
09.04.2013
##plugins.themes.bootstrap3.article.main##
Abstract
In the paper technical systems with counters are considered as logical models. The questions of formalization in temporal logic and automatic analysis via computational tree transformations are discussed.
##plugins.generic.usageStats.downloads##
##plugins.generic.usageStats.noStats##
##plugins.themes.bootstrap3.article.details##
How to Cite
Nepeivoda A. Technical systems in logic: questions of formalization and automatic verification // Logicheskie Issledovaniya / Logical Investigations. 2013. VOL. 19. C. 148-165.
Issue
Section
Papers
References
Ahmed, A., Lisitsa, A., and A.P. Nemytykh, Cryptographic Protocol Verification via Supercompilation. Reachability Problems, 2012. To appear.
Clarke, E.M., Emerson, E.A., and A.P. Sistla, Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM Transactions on Programming Languages and Systems 8(2):244–263, 1986.
Demri, S., Lazic, R., and A. Sangnier, Model Checking Freeze LTL over One-Counter Automata, Foundations of Software Science and Computational Structures, LNCS 4962:490–504, 2008.
Gluck, R., and A.V. Klimov, Occam’s razor in metacomputation: the notion of a perfect process tree, Static Analysis (Proc. Third International Workshop WSA’93), LCNS, 724:112–123, 1993.
Hamilton, G.W., Extracting the Essence of Distillation, Proceedings of the 7th PSI, Novosibirsk, Russia, LNCS, 5947:151–164, 2009.
Hamilton, G.W., and N.D. Jones, Distillation with labelled transition systems, PEPM, 2012, pp. 15–24.
Klimov, A.V., A Java Supercompiler and its Application to Verification of Cache-Coherence Protocols, PSI 2009. LNCS 5947:185–192, 2010.
Lisitsa, A., and A.P. Nemytykh, Verification as a parametrized testing (experiments with the SCP4 supercompiler), In Programming and Computer Software 33(1):14–23, 2007.
Lisitsa, A., and A.P. Nemytykh, Reachability Analysis in Verification via Supercompilation, Int. J. Found. Comput. Sci. 19(4):953–969, 2008.
Nemytykh, A.P., The SCP4 supercompiler: general structure, Moscow, 2007. 152 p. (in Russian).
Nepeivoda, A., Verification of a technical system model with linear temporal logic, Automation and Remote Control 93(9):124–140, 2012.
Secher, J.P., and M.H. S_rensen, On Perfect Supercompilation, Perspectives of System Informatics, LNCS 1755:113–127, 2000.
S_rensen, M.H., and R. Gluck, An algorithm of generalization in positive supercompilation, Logic Programming: Proc. of the 1995 International Symposium, 1995, pp. 465–479.
S_rensen, M.H., Gluck, R., and N.D. Jones, A positive supercompiler, Journal of Functional Programming 6(6):811–838, 1996.
Turchin, V.F., The concept of supercompiler, ACM Transactions on Programming Languages and Systems 8:292–325, 1986.
Patent No. 2367819, Russian Federation. MPC F04B 13/00 F17D 3/12 Publ. March 21, 2008. A method and construction for reagent dozing / F.F. Chausov.
Clarke, E.M., Emerson, E.A., and A.P. Sistla, Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM Transactions on Programming Languages and Systems 8(2):244–263, 1986.
Demri, S., Lazic, R., and A. Sangnier, Model Checking Freeze LTL over One-Counter Automata, Foundations of Software Science and Computational Structures, LNCS 4962:490–504, 2008.
Gluck, R., and A.V. Klimov, Occam’s razor in metacomputation: the notion of a perfect process tree, Static Analysis (Proc. Third International Workshop WSA’93), LCNS, 724:112–123, 1993.
Hamilton, G.W., Extracting the Essence of Distillation, Proceedings of the 7th PSI, Novosibirsk, Russia, LNCS, 5947:151–164, 2009.
Hamilton, G.W., and N.D. Jones, Distillation with labelled transition systems, PEPM, 2012, pp. 15–24.
Klimov, A.V., A Java Supercompiler and its Application to Verification of Cache-Coherence Protocols, PSI 2009. LNCS 5947:185–192, 2010.
Lisitsa, A., and A.P. Nemytykh, Verification as a parametrized testing (experiments with the SCP4 supercompiler), In Programming and Computer Software 33(1):14–23, 2007.
Lisitsa, A., and A.P. Nemytykh, Reachability Analysis in Verification via Supercompilation, Int. J. Found. Comput. Sci. 19(4):953–969, 2008.
Nemytykh, A.P., The SCP4 supercompiler: general structure, Moscow, 2007. 152 p. (in Russian).
Nepeivoda, A., Verification of a technical system model with linear temporal logic, Automation and Remote Control 93(9):124–140, 2012.
Secher, J.P., and M.H. S_rensen, On Perfect Supercompilation, Perspectives of System Informatics, LNCS 1755:113–127, 2000.
S_rensen, M.H., and R. Gluck, An algorithm of generalization in positive supercompilation, Logic Programming: Proc. of the 1995 International Symposium, 1995, pp. 465–479.
S_rensen, M.H., Gluck, R., and N.D. Jones, A positive supercompiler, Journal of Functional Programming 6(6):811–838, 1996.
Turchin, V.F., The concept of supercompiler, ACM Transactions on Programming Languages and Systems 8:292–325, 1986.
Patent No. 2367819, Russian Federation. MPC F04B 13/00 F17D 3/12 Publ. March 21, 2008. A method and construction for reagent dozing / F.F. Chausov.