时间区间时序逻辑模型检测：理论、算法及应用
|
摘要
行为、事件具有实时关系的软件或硬件系统构成了实时(计算)系统。在交通控制,航空航天等一系列对安全性要求极高的应用领域,实时系统的形式化验证成为保证系统正确性的重要手段。实时模型检测就是其中的一类自动验证方法,原理是实时逻辑公式描述系统所需满足的性质,时间自动机建立系统模型,验证算法自动判定模型是否满足性质。实时逻辑有很多种,用于形式化描述与验证也各有其优势,时间区间时序逻辑就是其中的一种线性实时逻辑,并已被应用于对一些实时系统的形式化描述与分析中。虽然该逻辑有其独特的比较优势,然而到目前为止,时间区间时序逻辑还不能用于实时系统的模型检测,因为缺少验证方法,也没有支撑方法的形式化理论来加深人们对该逻辑的理解和认识。针对于此,本文研究命题部分的时间区间时序逻辑模型检测问题,以该问题为主线,从理论、方法、应用三个层面构建其体系。
为了搞清楚该逻辑可以描述哪些性质、是否可应用于模型检测以及模型检测的效率,本文分别从逻辑的表达能力、判定性及复杂性三个方面进行研究,从而形成该逻辑模型检测的形式化理论。证明了离散时间域上的该逻辑与离散时间正则表达式、离散时间自动机等价,结果表明一切离散时间正则语言均可由离散时间区间时序逻辑加以形式化的描述。证明了稠时间逻辑其满足性不可判定,但存在其子集可判定,证明了离散时间逻辑满足性可判定,结果表明离散时间语义下该逻辑可模型检测。证明了问题固有复杂度为非初等,这表明人们所能开发出的最优工具在最坏情况下模型检测需时非初等,且分析表明最坏情况很难实际出现。
为了得到该逻辑模型检测的具体可操作方法,我们提出了一种新的计算模型---时间正则图。首先把逻辑公式转化为时间正则图,使得公式模型与图中路径一一对应。其次在图中添加接受条件即为性质时间自动机。最后性质自动机与模型自动机求交判空即为模型检测结果。这样就得到了基于时间正则图的离散时间区间时序逻辑模型检测算法。复杂度分析表明,新算法复杂度达到问题固有复杂度下限。针对样本公式的仿真结果表明,新方法在生成图状态空间方面优于对同类逻辑验证的现有方法。同时新方法也可推广到包括离散时段演算等同类逻辑模型检测中,我们给出了这样的推广算法。
为了避免普通模型检测方法从逻辑公式到自动机的复杂转换,我们发现了一种使用时间区间时序逻辑公式建立系统模型的方法,使用另一个该逻辑公式描述性质,这样统一模型检测问题就被归约为本文研究已解决的该逻辑公式满足性判定问题。与普通模型检测方法相比,新方法有利于实时计算系统开发中从规范到实现的逐步细化与求精。
为了提高误用入侵检测对实时攻击与并发攻击的描述能力与检测能力,我们提出了一种基于时间区间时序逻辑模型检测的入侵检测方法。首先使用该逻辑的公式描述不同攻击模式的签名,其次使用时间自动机建立日志库模型,最后模型检测算法自动验证自动机是否满足公式,即日志记录是否与攻击模式相符。仿真结果表明,与现有的基于模型检测的入侵检测方法相比,新方法可更有效地检测多种形式的telnet攻击和口令攻击。
Real-time systems are constituted of software or hardware systems that have real-time constraints. In the safety-critical systems, such as transport control systems, spaceflight and nuclear react control systems, model checking is a vital formal technique for guarantee correctness of real-time systems. The principles of this method are: describe the properties of a system with some real-time logic formulas, construct system models with timed automata, model checking algorithm decides automatically whether the models satisfy the properties. Several real-time logics including timed interval temporal logic (TITL) have been presented for formal verification. As a linear real-time logic, TITL has been used widely due to its advantages. But until now, TITL model checking problem has not been solved due to its absence of verification technique and formal theory. To this end, this paper investigates propositional TITL model checking problem as well as constructs its architecture on theory, method and application.
In order to make clear what kind of properties can be described by TITL, whether TITL can be used to model checking or not, and the efficiency of TITL model checking, we study expressive power, decidability and complexity of the logic. We prove the equivalence relation between discrete TITL formulas, discrete timed regular expressions and discrete timed automata. So, all of discrete timed regular language can be described and verified by TITL formulas. We prove its satisfiability is not decidable in the dense time domain, but there exists some subsets of full version of the logic that can be decidable. And we prove full version of the logic can be decided in the discrete time domain. So, TITL model checking problem is decidable. We also prove TITL satisfiability checking is a non-elementary problem. As shown in the analysis, not operation and chop operation are embedded interleaved in the worst case, but the probability is very low. So, non-elementary complexity affects scarcely applications of TITL model checking.
For automatic verification, we present a novel computational model named with timed normal form graph (TNFG). The fist step is to translate a TITL formula into a TNFG in order that there exists a one-to-one mapping between models of the formula and paths of the TNFG. The second step is to append accepting conditions to the TNFG in order to obtain the timed automaton modeling the TITL formula. The final step is to compute conduct automaton of two timed automata and decide whether the conduct automaton accept empty language or not. So, we obtain an algorithm for discrete TITL model checking based on TNFG. As shown in the complexity, our new algorithm reaches the lowest bound of inhabit problem complexity. As shown in the simulation results for some sample formulas, compared with the existing approaches, the new algorithm can produce lower state-space. And what’s more, we give an algorithm for translating formulas in a subset of discrete duration calculus (DC) into discrete TITL formulas. So, model checking this subset of discrete DC can be solved with TNFG.
In order to avoid complicated transformation from logic formulas to automata, we find an approach for unified TITL model checking. The first step is to construct a system model by a TITL formula. The second step is to describe a property with another TITL formula. So, unified TITL model checking problem is deduced to satisfiability checking problem that has been solved in this paper. Compared with common model checking techniques, the unified technique is benefit for refinement of real-time systems.
In order to raise the describing power of real-time attacks and concurrent attacks, we present an approach for intrusion detection based on TITL model checking. The first step is to describe attack patterns with TITL formulas. The second step is to construct an audit log by automata. The final step is to verify automatically whether automata satisfy formulas, i.e. the log match the attack patterns, by TITL model checking algorithm. As shown in the simulation results, compared with the existing approaches for intrusion detection based on model checking, our new approach can detect efficiently various telnet attacks and password attacks.
为了搞清楚该逻辑可以描述哪些性质、是否可应用于模型检测以及模型检测的效率,本文分别从逻辑的表达能力、判定性及复杂性三个方面进行研究,从而形成该逻辑模型检测的形式化理论。证明了离散时间域上的该逻辑与离散时间正则表达式、离散时间自动机等价,结果表明一切离散时间正则语言均可由离散时间区间时序逻辑加以形式化的描述。证明了稠时间逻辑其满足性不可判定,但存在其子集可判定,证明了离散时间逻辑满足性可判定,结果表明离散时间语义下该逻辑可模型检测。证明了问题固有复杂度为非初等,这表明人们所能开发出的最优工具在最坏情况下模型检测需时非初等,且分析表明最坏情况很难实际出现。
为了得到该逻辑模型检测的具体可操作方法,我们提出了一种新的计算模型---时间正则图。首先把逻辑公式转化为时间正则图,使得公式模型与图中路径一一对应。其次在图中添加接受条件即为性质时间自动机。最后性质自动机与模型自动机求交判空即为模型检测结果。这样就得到了基于时间正则图的离散时间区间时序逻辑模型检测算法。复杂度分析表明,新算法复杂度达到问题固有复杂度下限。针对样本公式的仿真结果表明,新方法在生成图状态空间方面优于对同类逻辑验证的现有方法。同时新方法也可推广到包括离散时段演算等同类逻辑模型检测中,我们给出了这样的推广算法。
为了避免普通模型检测方法从逻辑公式到自动机的复杂转换,我们发现了一种使用时间区间时序逻辑公式建立系统模型的方法,使用另一个该逻辑公式描述性质,这样统一模型检测问题就被归约为本文研究已解决的该逻辑公式满足性判定问题。与普通模型检测方法相比,新方法有利于实时计算系统开发中从规范到实现的逐步细化与求精。
为了提高误用入侵检测对实时攻击与并发攻击的描述能力与检测能力,我们提出了一种基于时间区间时序逻辑模型检测的入侵检测方法。首先使用该逻辑的公式描述不同攻击模式的签名,其次使用时间自动机建立日志库模型,最后模型检测算法自动验证自动机是否满足公式,即日志记录是否与攻击模式相符。仿真结果表明,与现有的基于模型检测的入侵检测方法相比,新方法可更有效地检测多种形式的telnet攻击和口令攻击。
Real-time systems are constituted of software or hardware systems that have real-time constraints. In the safety-critical systems, such as transport control systems, spaceflight and nuclear react control systems, model checking is a vital formal technique for guarantee correctness of real-time systems. The principles of this method are: describe the properties of a system with some real-time logic formulas, construct system models with timed automata, model checking algorithm decides automatically whether the models satisfy the properties. Several real-time logics including timed interval temporal logic (TITL) have been presented for formal verification. As a linear real-time logic, TITL has been used widely due to its advantages. But until now, TITL model checking problem has not been solved due to its absence of verification technique and formal theory. To this end, this paper investigates propositional TITL model checking problem as well as constructs its architecture on theory, method and application.
In order to make clear what kind of properties can be described by TITL, whether TITL can be used to model checking or not, and the efficiency of TITL model checking, we study expressive power, decidability and complexity of the logic. We prove the equivalence relation between discrete TITL formulas, discrete timed regular expressions and discrete timed automata. So, all of discrete timed regular language can be described and verified by TITL formulas. We prove its satisfiability is not decidable in the dense time domain, but there exists some subsets of full version of the logic that can be decidable. And we prove full version of the logic can be decided in the discrete time domain. So, TITL model checking problem is decidable. We also prove TITL satisfiability checking is a non-elementary problem. As shown in the analysis, not operation and chop operation are embedded interleaved in the worst case, but the probability is very low. So, non-elementary complexity affects scarcely applications of TITL model checking.
For automatic verification, we present a novel computational model named with timed normal form graph (TNFG). The fist step is to translate a TITL formula into a TNFG in order that there exists a one-to-one mapping between models of the formula and paths of the TNFG. The second step is to append accepting conditions to the TNFG in order to obtain the timed automaton modeling the TITL formula. The final step is to compute conduct automaton of two timed automata and decide whether the conduct automaton accept empty language or not. So, we obtain an algorithm for discrete TITL model checking based on TNFG. As shown in the complexity, our new algorithm reaches the lowest bound of inhabit problem complexity. As shown in the simulation results for some sample formulas, compared with the existing approaches, the new algorithm can produce lower state-space. And what’s more, we give an algorithm for translating formulas in a subset of discrete duration calculus (DC) into discrete TITL formulas. So, model checking this subset of discrete DC can be solved with TNFG.
In order to avoid complicated transformation from logic formulas to automata, we find an approach for unified TITL model checking. The first step is to construct a system model by a TITL formula. The second step is to describe a property with another TITL formula. So, unified TITL model checking problem is deduced to satisfiability checking problem that has been solved in this paper. Compared with common model checking techniques, the unified technique is benefit for refinement of real-time systems.
In order to raise the describing power of real-time attacks and concurrent attacks, we present an approach for intrusion detection based on TITL model checking. The first step is to describe attack patterns with TITL formulas. The second step is to construct an audit log by automata. The final step is to verify automatically whether automata satisfy formulas, i.e. the log match the attack patterns, by TITL model checking algorithm. As shown in the simulation results, compared with the existing approaches for intrusion detection based on model checking, our new approach can detect efficiently various telnet attacks and password attacks.
引文
[1] B Moszkowski, Reasoning about Digital Circuits. PhD thesis, Department of Computer Science, Stanford University, 1983
[2] H Bowman, S Thompson, A Decision Procedure and Complete Axiomatization of Finite Interval Temporal Logic with Projection, Journal of Logic and Computation, 13(2):195-239, 2003
[3] Z Duan, Temporal Logic and Temporal Logic Programming, Beijing: Science Press, 2005
[4] Z Duan, etc, Projection in temporal logic programming, Proceedings of 5th International Conference on Logic Programming and Automated Reasoning, Lecture Notes in Computer Science 822, Springer,pages 333-344,1994.
[5] Z Duan, An Extended Interval Temporal Logic and a Framing Technique for Temporal Logic Programming, PhD thesis, Department of Computing Science, University of Newcastle Upon Tyne, May 1996. Technical report 556
[6] Z Duan, X Yang, M Koutny, Framed temporal logic programming, Science of Computer Programming, 70(1):31-61,2008
[7] Z Duan, M A Koutny, Framed Temporal Logic Programming Language, Journal of Computer Science and Technology, 19(3):341-351,2004.
[8] B Moszkowski, Compositional reasoning about projected and infinite time, In Proceedings of the First IEEE International Conference on Engineering of Complex Computer Systems (ICECCS’95), pages 238–245. IEEE Computer Society Press, 1995
[9] Z Duan, C Tian, L Zhang, A decision procedure for propositional projection temporal logic with infinite models, Acta Informatica, 45(1):43-78, 2008
[10] L Stockmeyer, The Complexity of Decision Problems in Automata Theory and Logic, Ph.D. thesis, MIT,1974
[11] E M Clarke, etc, Model checking, Massachusetts: MIT press, 1999
[12] R Alur, D L Dill, A Theory of Timed Automata, Theoretical Computer Science, 126(2): 183-236, 1994
[13] R Alur, T Feder, T A Henzinger, The benefits of relaxing punctuality, Journal of the ACM, 43(1):116～146, 1996
[14] R Alur, T A Henzinger, A really temporal logic, Journal of the ACM, 41(1):181～204, 1994
[15] C Tian, Z Duan, Model Checking Propositional Projection Temporal Logic Based on SPIN, ICFEM2007, LNCS4789, pp. 246-265, Springer, Heidelberg , 2007
[16] R Alur, T A Henzinger, Logics and models of real time: A survey, Lecture Notes in Computer Science, 600. Springer-Verlag, 74～106, 1992
[17] T Wilke, Specifying timed state sequences in powerful decidable logics and timed automata, Lecture Notes in Computer Science, 863, pp. 694-715, 1994
[18] T A Henzinger, Z Manna, A Pnueli, What good are digital clocks?, In Proc. ICALP’92, volume 623 of LNCS, pages 545–558. Springer, 1992
[19] Z Duan, Modeling of hybrid system, Ph.D thesis, UK: Department of Computer Science, University of Shefield, 1997
[20] Z Duan, Modeling of hybrid systems, Beijing: science press,2004
[21] C Zhou, C A Hoare, A P Ravn, A calculus of durations, Information Processing Letters, 40(5): 269-276, 1991
[22] M Fr?nzle, Model-checking dense-time duration calculus, Formal Aspects of Computing, 16 (2):121-139, 2004
[23] M R Hanson, Model-checking discrete duration calculus, Formal Aspects of Computing, 6A:826-845, 1994.
[24] Z Duan, C Tian, Decidability of Propositional Projection Temporal Logic with Infinite Models, The 4th Annual Conference on Theory and Applications of Models of Computation, shanghai, China, 2007, (NO.377), LNCS, Springer.
[25] C Zhou, M R Hansen, P Sestoft, Decidability and Undecidability Results for Duration Calculus, STACS'93, vol. 665, pp. 58-68, Springer-Verlag, 1993.
[26] G Li, Z Tang, Translating a Continuous-Time Temporal Logic into Timed Automata, Proceedings of the first Asian Symposium on Programming Languages and Systems (APLAS 2003), Lecture Notes in Computer Science 2895, pp.322--338, Springer-Verlag, 2003
[27] L Lamport, The temporal logic of actions, ACM Transactions on programming language and systems,16(3):872-923,1994.
[28] S Demri, P Schnoebelen, The complexity of propositional linear temporal logics in simple cases, Information and Computation, 174(1):84–103, 2002.
[29] C Tian, Z Duan, Propositional Projection Temporal Logic, Büchi Automata and omega-Regular Expressions, in Proceedings, Theory and Applications of Models of Computation, Lecture Notes in Computer Science, 4978, Springer, 2008:47-58.
[30] C Petri, Kommunikation mit Automaten (Communication with Automata), PhD thesis, Technische Universitat Darmstadt, Germany, 1962
[31] M Roger, J Goubault-Larrecq, Log Auditing through Model-Checking, Proceedings of the 14th IEEE workshop on Computer Security Foundations, IEEE Computer Society Washington, DC, USA, 220-234, 2001.
[32] G T Rohrmair, G Lowe, Using data-independence in the analysis of intrusion detection systems, Theoretical Computer Science, 340(1):82-101, 2005.
[33] O Sheyner, J Haines, S Jha, etc, Automated generation and analysis of attack graphs, Proceedings of the 2002 IEEE Symposium on Security and Privacy, 273-284, 2004.
[34] Z Nan, R Mark, P G Dimitar, Evaluating Access Control Policies Through Model Checking, Lecture Notes in Computer Science, Information Security, Springer Berlin, 3650:446-460, 2005.
[35] S Sebastian, V Michael, K Hartmut, Identifying Modeling Errors in Signatures by Model Checking, Lecture Notes in Computer Science, Model Checking Software, Springer Berlin, 5578:205-222, 2009.
[36] J Olivain, J Goubault-Larrecq, The ORCHIDS Intrusion Detection Tool, Proceedings of the 17th International Conference on Computer Aided Verification, Lecture Notes in Computer Science, 3576:286-290, Springer, Edinburgh, Scotland, UK, 2005.
[37] C Tian, Z Duan, Complexity of propositional projection temporal logic with star, Mathematical Structures in Computer Science, 19(1):73-100, 2009
[38] V Goranko, A Montanari, G Sciavicco, A Road Map of Interval Temporal Logics and Duration Calculi, Journal of Applied Non-Classical Logics, 14(1-2): 9-54, 2004
[39] M Hira, D Sarkar, Verification of Tempura Specification of Sequential Circuits, IEEE Trans. on CAD of Integrated Circuits and Systems, 16(4):362-375, 1997.
[40] A Cau, H Zedan, A Coleman, et al, Using ITL and Tempura for Large Scale Specification and Simulation, Proceeding of 4th Euro-micro Workshop on Parallel and Distributed Processing. IEEE Computer Society Press, 493-500,1996
[41] M Solanki, S Tesco, A Framework for Defining Temporal Semantics in Owl Enabled Services, Proceeding of W3C Workshop on Frameworks for Semantics in Web Services. 1-6, 2005.
[42] M Solanki, A Cau, H Zedan, Semantically Annotating Reactive Web Services with Temporal Specifications, Proceedings of the IEEE ICWS 2005, Second International Workshop on Semantic and Dynamic Web Processes. 2005.
[43] Z Duan, L Zhang, A Decision Procedure for Propositional Projection Temporal Logic, Technical Report No.1, Institute of computing Theory and Technology, Xidian University, Xi'an P.R.China, 2005
[44]唐稚松,时序逻辑程序与软件工程,北京:科学出版社,2002。
[45]李广元,唐稚松,带有时钟变量的线性时序逻辑与实时系统验证,软件学报,13(1):33-41,2002
[46]李广元,唐稚松,基于线性时序逻辑的实时系统模型检查,软件学报,13(2):193-202,2002
[47]朱一清,可计算性和计算复杂性,北京:国防工业出版社,2006。
[48]张燕、傅建明、孙晓梅,一种基于模型检查的入侵检测方法,武汉大学学报(理学版),51(3):319-322,2005。
[49] E Clarke, O Grumberg, D Long, Verification Tools for Finite-State Concurrent Systems, A Decade of Concurrency-Reflections and Perspectives, LNCS 803, 124-175, 1993
[50] U Stern, D Dill, A New Scheme for Memory-Efficient Probabilistic Verification. In IFIP TC6/WG6.1 Joint International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols, and Protocol Specification, Testing, and Verification, 333-348, 1996.
[51] P Godefroid, G Holzmann, D Pirottin, State-space caching revisited, Formal Methods in System Design, 7(3):227– 241,1995.
[52] D Peled, Combining Partial Order Reductions with On-the-Fly Model-Checking, Formal Methods in System Design, 8(1):39-64, 1996
[53] D Peled, T Wilke, Stutter-invariant temporal properties are expressible without the next-time operator, Information Processing Letters, 63(5):243-246, 1997
[54] D Dams, O Grumberg, R Gerth, Abstract Interpretation of Reactive Systems. ACM Transactions on Programming Languages and Systems, 19(2), 253-291, 1997
[55] A Sistla, E Clarke, The complexity of propositional linear temporal logics, Journal of the ACM, 32(3):733-749, 1985
[56] P Schnoebelen, The complexity of temporal logic model checking, Proceedings of the 4th. Conference Advances in Modal Logic, vol. 4, pp. 437-459, King's CollegePublication, 2003,
[57] G Holzmann, The model checker SPIN, IEEE Transactions on Software Engineering, 23(5):279-295, 1997
[58] M Vardi, An automata-theoretic approach to linear temporal logic, Proceedings of the VIII Banff Higher order workshop conference on Logics for concurrency : structure versus automata: structure versus automata, 238-266,1996.
[59] A Gurfinkel, O Wei, M Chechik, Systematic Construction of Abstractions for Model-Checking. In 7th Verification, Model Checking, and Abstract Interpretation, LNCS 3855, pages 381–397. Springer-Verlag, 2006.
[60] J Esparza, K Heljanko, A New Unfolding Approach to LTL Model Checking, Lecture Notes in Computer Science, Automata, Languages and Programming, Springer Berlin/Heidelberg, Volume 1853/2000,page 475-486,2000
[61] P Gastin, D Oddoux, Fast LTL to Büchi Automata Translation, Lecture Notes in Computer Science, Computer Aided Verification, Springer Berlin / Heidelberg, Volume 2102/2001,53-65,2001
[62] M Hammer, A Knapp, S Merz, Truly On-the-Fly LTL Model Checking, Lecture Notes in Computer Science, Tools and Algorithms for the Construction and Analysis of Systems, Springer Berlin/Heidelberg, Volume 3440/2005, 191-205, 2005
[63] S Yovine, Model checking timed automata, In Lectures on Embedded Systems, LNCS 1494, pages 114-152. Springer-Verlag, October 1998.
[64] H M Lin, Y Wang, Axiomatising timed automata, Acta Informatica, 38(4): 277–305, 2002.
[65] Markus Muller-Olm, David Schmidt, Bernhard Steffen, Model Checking A Tutorial Introduction. SAS'99, LNCS 1694, pp. 330-354, 1999.
[66] R Gerth, D Peled, M Y Vardi, Simple On-the-fly Automatic Verification of Linear Temporal Logic, In Protocol Specification Testing and Verification, Chapman & Hall, 3-18, 1995.
[67] A He, J Wu, L Li, An Efficient Algorithm for Transforming LTL Formula to Büchi Automaton, 2008 International Conference on Intelligent Computation Technology and Automation (ICICTA), 1215-1219,2008.
[68] C Fritz, Constructing Büchi automata from linear temporal logic using simulation relations for alternating Büchi automata, Proceedings of the 8th international conference on Implementation and application of automata, Lecture Notes In Computer Science, Springer-Verlag, Berlin, Heidelberg, 35-48, 2003.
[69] K Etessami, Temporal massage parlor. http://www1.bell-labs.com/ project/TMP/. 36, 37, 43.
[70] M Daniele, F Giunchiglia, M Vardi, Improved Automata Generation for Linear Temporal Logic, Proceedings of the 11th International Conference on Computer Aided Verification, Lecture Notes In Computer Science, 1633, Springer-Verlag, London, UK, 249 - 260, 1999.
[71] F Somenzi, R Bloem, Efficient Büchi Automata from LTL Formulae, Proceedings of the 12th International Conference on Computer Aided Verification, Lecture Notes In Computer Science, 1855, Springer-Verlag, London, UK, 248,263, 2000.
[72] D Giannakopoulou, F Lerda, Efficient translation of LTL formulae into Büchiautomata, RIACS, Technical Report, 01.29, June 2001.
[73] D Giannakopoulou, F Lerda, From States to Transitions: Improving Translation of LTL Formulae to Büchi Automata, Proceedings of the 22nd IFIP WG 6.1 International Conference Houston on Formal Techniques for Networked and Distributed Systems, Lecture Notes in Computer Science 2529, 308– 326, Springer-Verlag, London, UK, 2002.
[74] M D Wulf, L Doyen, N Maquet, Antichains: Alternative Algorithms for LTL Satisfiability and Model-Checking, Proceedings of TACAS 2008, LNCS 4693, 63-77, Springer-Verlag, Budapest, 2008.
[75] R Bloem, K Ravi, F Somenzi, Efficient decision procedures for model checking of linear time logic properties, In Proceedings of the 11th International Conference on Computer Aided Verification, LNCS 1633, pages 222-235, Springer-Verlag, London, UK,1999.
[76] P Wolper, Constructing Automata from Temporal Logic Formulas : A. Tutorial. Springer Lectures On Formal Methods And Performance Analysis, 261-277, Lectures on formal methods and performance analysis: first EEF/Euro summer school on trends in computer science, Springer-Verlag, New York, 2002.
[77] Ouyang Ming-Guang, Pan Feng, Zhang Yun-Tao, ISITL: Intrusion signatures in augmented interval temporal logic, International Conference on Machine Learning and Cybernetics, v 3, p 1630-1635, 2003
[78] Elzbieta Nowicka, Marcin Zawada, An Interval Temporal Logic-Based Matching Framework for Finding Occurrences of Multi-event Attack Signatures, Computer Network Security, Communications in Computer and Information Science, Volume 1, Part 5, Part 8, 272-285, 2007.
[79] Ouyang Ming-Guang, Zhou Yang-Bo, ISDTM: An intrusion signatures description temporal model, Wuhan University Journal of Natural Sciences, v 8, n 2 A, p 373-378, 2003.
[80] Pratt-Hartmann Ian, Temporal prepositions and their logic, Artificial Intelligence, v 166, n 1-2, p 1-36, 2005.
[81]张琳琳、应时、倪友聪、等,一种软件体系结构关注点分析方法,计算机学报,32(9):1782-1791,2009。
[82] Konur Savas, A decidable temporal logic for events and states, Proceedings of the International Workshop on Temporal Representation and Reasoning, v 2006, p 36-41, 2006.
[83] J R Buchi, On a decision method in restricted second order arithmetic, In Proceedings of the International Congress on Logic, Method, and Philosophy of Science, pages 1-12. Stanford University Press, 1962.
[84] Janicke Helge, Cau Antonio, Siewe Fran?ois, etc, A compositional event & time-based policy model, Seventh IEEE International Workshop on Policies for Distributed Systems and Networks, Policy 2006, IEEE Computer Society, v 2006, p 173-182, 2006.
[85] Pandya, K Paritosh, The saga of synchronous bus arbiter: On model checking quantitative timing properties of synchronous programs, Electronic Notes in Theoretical Computer Science, v 65, n 5, p 894-908, July 2002.
[86] Kazhamiakin Raman, Pandya Paritosh, Pistore Marco, Timed modelling and analysis in Web service compositions, First International Conference on Availability, Reliability and Security, ARES 2006, IEEE Computer Society, v 2006, p 840-846, 2006.
[87] Kazhamiakin Raman, Pandya Paritosh, Pistore Marco, Representation, verification, and computation of timed properties in Web service compositions, IEEE International Conference on Web Services, IEEE Computer Society, p 497-504, 2006.
[88] Ruggero Lanotte, Andrea Maggiolo-Schettini, Simone Tini, Concurrency in timed automata, Theoretical Computer Science, 309(1-3): 503-527, 2003.
[89]张海宾、段振华,区间时序逻辑的模型检查,西安电子科技大学学报(自然科学版),36(2):338-342,2009
[90]张海宾、段振华,稠密时间区间时序逻辑的可满足性判定,西安电子科技大学学报(自然科学版),34(3):463-467,2009
[91]裴玉、徐启文、李宣东、等, QRDChecker:一个QRDC模型检验工具,软件学报,16(3):355-364,2005
[92]张海宾、段振华,多速率混合系统的模型检查,西安电子科技大学学报(自然科学版),35(1):60-64、86,2008
[93] H Ma, L Li, W Wang, etc, Automatic synthesis of the DC specifications of lip synchronisation protocol, Proceedings of the Asia-Pacific Software Engineering Conference and International Computer Science Conference, APSEC and ICSC, p 371-378, IEEE Computer Society, 2001.
[94]雷丽晖、段振华,使用扩展区间时序逻辑为并发工作流建模,西安电子科技大学学报(自然科学版),34(4):673-680,2007
[95] L Zhang, Combining formal specification methods and informal specification methods for requirement analysis, IEEE Pacific RIM Conference on Communications, Computers, and Signal Processing - Proceedings, v 1, p 444-447, 1997.
[96] B Moszkowski, Using temporal logic to analyse temporal logic: A hierarchical approach based on intervals, Journal of Logic and Computation, v 17, n 2, p 333-409, 2007.
[97] Pratt-Hartmann Ian, Temporal prepositions and their logic: Extended abstract, Proceedings of the International Workshop on Temporal Representation and Reasoning, v 11, p 7-8, 2004.
[98] B Dines(著),刘伯超(译),软件工程,北京:清华大学出版社,2010
[99] Bowman Howard, Faconti Giorgio, Analysing cognitive behaviour using LOTOS and Mexitl, Formal Aspects of Computing, v 11, n 2, p 132-159, 1999.
[100]王小兵、段振华,面向投影时序逻辑的Web服务模型检测,西安交通大学学报,43(4):39-43、124,2009。
[101]雷丽晖、段振华,基于扩展投影时序逻辑的组合Web服务描述与验证,西安交通大学学报,41(10):1155-1159,2007。
[102]舒新峰、段振华,利用投影时序逻辑的多内核进程调度建模与验证,西安交通大学学报,44(33):52-57,2010。
[103]舒新峰、段振华,投影时序逻辑的公理系统与形式验证,西安电子科技大学学报(自然科学版),36(4):680-685、729,2009。
[104]王小兵、段振华,框架投影时序逻辑程序设计语言中的指针,西安电子科技大学学报(自然科学版),35(6):1069-1074,2008。
[105]杨琛、段振华、王小兵,面向命题投影时序逻辑的安全协议模型检测,西安交通大学学报,44(8):30-35,2010。
[106] Z Duan, N Zhang, A complete axiomatization of Propositional Projection Temporal Logic, Proceedings - 2nd IFIP/IEEE International Symposium on Theoretical Aspects of Software Engineering, TASE 2008, p 271-278, 2008.
[107] Z Duan, C Tian, A unified model checking approach with projection temporal logic, Lecture Notes in Computer Science, v 5256 LNCS, p 167-186, 10th International Conference on Formal Engineering Methods, ICFEM 2008, Oct 27– 31, Verlag, 2008.
[108]王小兵、段振华,面向对象的时序逻辑语言,电子科技大学学报,38(1):97-101、107,2009。
[109] P Zhang, Z Duan, C Tian, UML statecharts' PTL formal semantics, 3rd International Symposium on Intelligent Information Technology Application, IITA 2009, v 1, p 381-385, IEEE Computer Society, 2009.
[110] Z Duan, X Yang, K Maciej, Semantics of framed temporal logic programs, Lecture Notes in Computer Science, 21st International Conference on Logic Programming, Springer Verlag, v 3668, p 356-370, 2005.
[111]张海宾,、段振华,混合系统的符号化可达性分析,软件学报,19(12):3111-3121,2008。
[112] H Zhang, Z Duan, Symbolic Algorithmic Analysis of Rectangular Hybrid Systems, Journal of Computer Science and Technology, 24(3):534-543, 2009.
[113]张海宾,、段振华,多速率混合系统的符号化可达性分析,西安交通大学学报,41(4):412-415,2007。
[114] C Tian, Z Duan, A note on stutter-invariant PLTL, Information Processing Letters, 109(13):663-667, 2009.
[115]王小兵,面向对象MSVL语言及其在组合Web服务验证中的应用,博士学位论文,西安:西安电子科技大学计算机学院,2009。
[116] X Yang, Formal Semantics of Framed Temporal Logic Programming Language MSVL, Ph.D thesis, Xi’an: School of Computer Science, Xidian University, P R China, 2009.
[117] H Zhang, Formal Verification of Hybrid Systems, Ph.D thesis, Xi’an: School of Computer Science, Xidian University, P R China, 2007.
[118] Z Duan, C Yang, Unconditional secure communication: a Russian Cards protocol, Journal of Combinatorial Optimization, 19(4): 501-530, 2010.
[119] Christel Baier,Joost-Pieter Katoen,Principles of Model Checking,The MIT Press,Cambridge, Massachusetts,London, England,2004
[120] Rodolfo Gomez, Howard Bowman, A MONA-based Decision Procedure for Propositional Interval Temporal Logic, Workshop of Interval Temporal Logics and Duration Calculi (part of the 15th European Summer School in Logic, Language and Information, August 2003. http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.2.3812&rep=rep1&type=pdf
[121]晏荣杰、李广元、徐雨波、等,有限精度时间自动机的可达性检测,软件学报,17(1):1-10,2006。
[122] Patricia Bouyer, Nicolas Markey, Jo?l Ouaknine, etc, On Expressiveness and Complexity in Real-time Model Checking, Proceedings of the 35th international colloquium on Automata Languages and Programming, Part II, 2008. http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.151.2670&rep=rep1&type=pdf
[123] Jo?l Ouaknine, Alexander Rabinovich, James Worrell, Time-Bounded Verification, Proceedings of CONCUR 09 (improved and expanded version), LNCS 5710, 19 pages, 2009. http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.153.6937&rep=rep1&type=pdf
[124] Dang Van Hung, Phan Hong Giang, A Sampling Semantics of Duration Calculus, Formal Techniques for Real-Time and Fault Tolerant Systems, LNCS 1135, Spriger-Verlag, 1996. http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.103.6577&rep=rep1&type=pdf
[125] Martin Franzle, Michael R Hansen, Efficient Model Checking for Duration Calculus, International Journal of Software Informatics, 3(2-3):171-196, 2009.
[126] V A Braberman, D V Hung, On Checking Timed Automata for Linear Duration Invariants, Proceedings of 19th the IEEE Real-Time Systems Symposium, 1998. http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.12.7174&rep=rep1&type=pdf
[127] Pham Hong Thai, Dang Van Hung, Verifying Linear Duration Constraints of Timed Automata, Theoretical Aspects of Computing - ICTAC 2004, Lecture Notes in Computer Science, Volume 3407/2005, 295-309, SPRINGER-VERLAG, Germany, 2005.
[128] D'Silva Vijay, Kroening Daniel,Weissenbacher Georg, A Survey of Automated Techniques for Formal Software Verification, IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 27(7): 1165-1178, 2008.
[129] Dennis Dams, Abstraction in Software Model Checking: Principles and Practice, Model checking software: 9th International SPIN Workshop, Vol 2318: 14-22, LNCS, Springer-Verlag, 2002.
[130] T Paul Darga, Chandrasekhar Boyapati, Efficient Software Model Checking of Data Structure Properties, Proceedings of the 21st annual ACM SIGPLAN conference on Object-oriented programming systems, languages, and applications, Volume 41 Issue 10, 363-382, October 2006
[131] Tevfik Bultan, Aysu Betin-Can, Scalable Software Model Checking Using Design for Verification, In Proceedings of the IFIP Working Conference on Verified Software: Theories, Tools, Experiments, Lecture Notes in Computer Science, Volume 4171/2008, 337-346, 2008.
[132] V Shobha, A Jacob. Abraham, Static program transformations for efficient software model checking, IFIP International Federation for Information Processing, Volume 156/2004, Building the Information Society, 257-281, 2004.
[133] Radu Iosif , Symmetry Reduction Criteria for Software Model Checking, Proceedings of the 9th International SPIN Workshop on Model Checking of Software, 22– 41, Springer-Verlag London, UK, 2002.
[134] Patrice Godefroid, Software model checking: the verisoft approach, Formal Methods in System Design, Volume 26, Number 2, 77-101, 2005.
[135] Patrice Godefroid, Software Model Checking Improving Security of a Billion Computers, Proceedings of the 16th International SPIN Workshop on Model Checking Software, Lecture Notes in Computer Science, Volume 5578/2009, 1-1, 2009.
[136]并发实时系统的理论与方法, http://lcs.ios.ac.cn/introduce/concurrency.htm, 2006.
[137]吴尽昭、王永祥、覃广平,交互式马尔可夫链——并发系统的设计、验证与评价(数学机械化丛书),北京:科学出版社,2007。
[138] Howard Bowman, Helen Cameron, Peter King, Mexitl: Multimedia in Executable Interval Temporal Logic, Formal Methods in System Design, Volume 22, Number 1, 5-38, 2003.
[139] Rodolfo Gómez, Howard Bowman, PITL2MONA: Implementing a Decision Procedure for Propositional Interval Temporal Logic, Journal of Applied Non-Classical Logics , Volume 14, Number 1-2, 105-148, 2004.
[140] James Glenn, William Gasarch, Implementing WS1S via Finite Automata, the First International Workshop on Implementing Automata, Lecture Notes in Computer Science, Volume 1260/1997, 50-63, 1997.
[141] E Asarin, P Caspi, O Maler, A Kleene theorem for timed automata, Proceedings of the 12th Annual IEEE Symposium on Logic in Computer Science, p.160-171, Warsaw , Poland, 1997.
[142] Eugene Asarin, Paul Caspi, Oded Maler, Timed Regular Expressions, Journal of the ACM, Volume 49 Issue 2, 172-206, 2002.
[143] Lange Martin, Temporal Logics for Non-Regular Properties Model Checking, Proc.\ 4th Int.\ Workshop on Methods for Modalities, HU Berlin, Berlin, Germany, 194:1-7, 2005.
[144] Julian Bradfield, Colin Stirling, Modal Mu-Calculi, Handbook of Modal Logic, Elsevier, 721-756, 2007. http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.143.9834&rep=rep1&type=pdf
[145] E Emerson, Model Checking and the Mu-calculus, Descriptive Complexity and Finite Models, American Mathematical Society, pp. 185–214, 1996. http://www.cs.utexas.edu/users/emerson/Pubs/1996-01.Em.mod-chk-and-mu-calc.ps
[146]林惠民、张文辉,模型检测:理论、方法与应用,电子学报,30(12A):1907-1912,2002。
[147] Slawomir Lasota, Igor Walukiewicz, Alternating timed automata, ACM Transactions on Computational Logic, 9(2): 1–26, 2008.
[148] Deepak D’Souza, M Raj Mohan, Eventual Timed Automata, In Foundations of Software Technology and Theoretical Computer Science, Lecture Notes in Computer Science, Volume 3821, 322-334, 2005
[149] B C Moszkowski, A complete axiomatization of interval temporal logic with infinite time, In. Proc. 15th Annual IEEE Symp. on Logic in Computer Science, 241-252, IEEE Computer Society Washington, DC, USA, 2002.
[150] B C Moszkowski, An automata-theoretic completeness proof for interval temporal logic, Proceedings of the 27th International Colloquium on Automata, Languages and Programming, 223-234, Springer-Verlag London, UK, 2000.
[151] B C Moszkowski, Compositional reasoning using interval temporal logic and tempura, International Symposium on Compositionality: The Significant Difference, Lecture Notes in Computer Science, Volume 1536, 439-464, 1998.
[152] A Cau, B Moszkowski, Using PVS for interval temporal logic proofs. Part 1: The syntactic and semantic encoding, Technical Monograph 14, SERCentre, De Montfort University, Leicester, 1996.
[153] A Zinoviev, ITL as a Language for Regular Relations, In: Proceedings of 4th Panhellenic. Loguc Symposium, 2003. http://www2.cs.ucy.ac.cy/projects/pls4/Zinoviev.ps
[154] D P Guelev, Van Hung, Prefix and projection onto state in duration calculus, Electronic Notes in Theoretical Computer Science, vol. 65, Elsevier Science Publishers, Amsterdam, 2002.
[155] He Jifeng, A Behavioral Model for Co-design, Proceedings of the Wold Congress on Formal Methods in the Development of Computing Systems-Volume II, p.1420-1438, September 20-24, 1999.
[156] Dang Van Hung, Projections: A Technique for Verifying Real-Time Programs in Duration Calculus. Technical Report 178, UNU-IIST, P.O. Box 3058, Macau, November 1999. Published in the proceedings of the Conference on Information Technology and Education, Ho Chi Minh City, Vietnam, January 2000.
[157] S Kono, A Combination of Clausal and Non Clausal Temporal Logic Program, IJCAI-93 Workshop on Executable Modal and Temporal Logics, Lecture Notes in Computer Science, Volume 897, 69-85, 1995.
[158] Howard Bowman, Simon Thompson, A tableau method for interval temporal logic, Technical report. University of Kent at Canterbury, 1997.
[159] Z Manna, A Pneuli, Verification of Concurrent Programs: The Temporal Framework, The Correctness Problem in Computer Science (R. S. Boyer and J. S. Moore, eds.), International Lecture Series in Computer Science, 1981. Also in Annals of Pure and Applied Logic, Volume 51, Issues 1-2, Pages 79-98, 1991.
[160] Akio Nakata, Teruo Higashino, Deriving parameter conditions for periodic timed automata satisfying real-time temporal logic formulas, 21st International Conference on Formal Techniques for Networked and Distributed Systems, 151-168, Kluwer, B.V. Deventer, The Netherlands, The Netherlands, 2001.
[161] Ahmed Bouajjani, Yassine Lakhnech, Sergio Yovine, Model checking for extended timed temporal logics, Proceedings of the 4th International Symposium onFormal Techniques in Real-Time and Fault-Tolerant Systems, 306-326, Springer-Verlag London, UK, 1996.
[162] Ahmed Bouajjani, Yassine Lakhnech, Temporal logic + timed automata: expressiveness and decidability, Proceedings of the 6th International Conference on Concurrency Theory, 531-545, Springer-Verlag London, UK, 1995.
[163] Z Duan, M Holcombe, Timed interval temporal logic and modelling of hybrid systems, in Proceedings of Modelling and Simulation ESM'94, Barcelona, Spain, June 1-3, pp. 534-41, 1994.
[164] Deutsche Forschungsgemeinschaft, Forderkennzeichen La, Martin Fr?nzle, Decidability of duration calculi on restricted model calsses, http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.12.105&rep=rep1&type=pdf, 1996.
[165] C Zhou, D V Hung, X Li, A duration calculus with infinite intervals, Proceedings of the 10th International Symposium on Fundamentals of Computation Theory, Lecture Notes in Computer Science, Volume 965, 16-41, 1995.
[166] C A R Hoare, Communicating sequential processes, Prentice Hall International Series in Computing Science, Prentice Hall, 1985. Also in http://www.usingcsp.com/cspbook.pdf
[167] G M Reed, A W Roscoe, A timed model for communicating sequential processes, Theoretical Computer Science, Volume 58 Issue 1-3, 249-261, 1988.
[168] Dan R Ghica, A games-based foundation for compositional software model checking, Ph.D thesis, Queen’s University, Kingston, Ontario, Canada, 2002.
[169]武新华,黑客命令与典型应用,北京:中国铁道出版社,2009。
[170] Glynn Winskel(著),宋国新、邵志清(译),程序设计语言的形式语义,北京:机械工业出版社,2004。
[171]王永祥、吴尽昭、蒋建民,进程代数---对称与动作细化,数学机械化丛书,北京:科学出版社,2007。
[172]古天龙,软件开发的形式化方法,北京:高等教育出版社,2005。
[173] J邦詹森、G古廷(著),姚兵、张忠辅(译),有向图的理论、算法及其应用,北京:科学出版社,2009。
[174] T A Henzinger, The Temporal Specification and Verification of Real-Time Systems, PhD thesis, Stanford University, August 1991.
[175] Joost-Pieter Katoen, Concepts, algorithms and tools for model checking, 1999. http://www.cs.aau.dk/~kgl/VERIFICATION99/katoen2.ps
[176] L Gonnord, N Halbwachs, P Raymond, From discrete duration calculus to symbolic automata, In 3rd International Workshop on Synchronous Languages, Applications, and Programs, SLAP’04, Barcelona, Spain, March 2004. Also in Electronic Notes in Theoretical Computer Science (ENTCS), Volume 153 Issue 4, 3-18, June, 2006.
[177] F Pieniazek, V Braberman, On Checking Finitary Timed Automata for Duration Properties, Tech. Rep. UBA, TR99-007, 1999. http://www.dc.uba.ar/people/proyinv/tr.html
[178] Alexander Rabinovich, On expressive completeness of duration and mean value calculi, Theoretical Computer Science, Volume 230 Issue 1-2, 2000.http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.38.5393&rep=rep1&type=ps
[179] X Li, Decidability of Mean Value Calculus, Journal of Computer Science and Technology, 14(2): 173-180, 1999.
[180] Ben Moszkowski, Benefits of Interval Temporal Logic for Specification of Concurrent Systems, http://www.cl.cam.ac.uk/~md466/ccw2010/moszkowski-temporal.pdf, 2010.
[181] Z Duan, M Holcombe, A hybrid projection temporal logic for hybrid systems, http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.54.9022&rep=rep1&type=pdf, 1998.
[182] Michael Reichhardt Hansen, Dang Van Hung, A Theory of Duration Calculus with Application, Domain Modeling and the Duration Calculus, Lecture Notes in Computer Science, Volume 4710, 119-176, 2007.
[183] Y LI, D V Hung, Checking temporal duration properties of timed automata, Journal of Computer Science and Technology, Volume 17 Issue 6, 689-698, November 2002.
[184] Michael R Hansen and Zhou Chaochen, Duration calculus logical foundations, Formal Aspects of Computing, Volume 9, Number 3, 283-330, 1997.
[185] D Guelev, Logical Interpolation and Projection onto State in the Duration Calculus, Journal of Applied Non-classical Logics, 14(1-2): 181-208, 2004.
[186] Roland Meyer, Johannes Faber, Andrey Rybalchenko, Model checking Duration Calculus a practical approach, Formal Aspects of Computing, Volume 20 Issue 4-5, 332-346, June 2008.
[187] Dimitar P Guelev, Dang Van Hung, On the completeness and decidability of duration calculus with iteration, Theoretical Computer Science, 337(1-3): 278-304, 2005.
[188] D V Hung, J Wang, On the design of hybrid control systems using automata models, Proceedings of the 16th Conference on Foundations of Software Technology and Theoretical Computer Science, Lecture Notes in Computer Science, Volume 1180, 156-167, 1996.
[189]侯建民、李宣东、郑国梁,离散时段演算的符号模型验证,计算机学报,21(2):103-110,1998。
[2] H Bowman, S Thompson, A Decision Procedure and Complete Axiomatization of Finite Interval Temporal Logic with Projection, Journal of Logic and Computation, 13(2):195-239, 2003
[3] Z Duan, Temporal Logic and Temporal Logic Programming, Beijing: Science Press, 2005
[4] Z Duan, etc, Projection in temporal logic programming, Proceedings of 5th International Conference on Logic Programming and Automated Reasoning, Lecture Notes in Computer Science 822, Springer,pages 333-344,1994.
[5] Z Duan, An Extended Interval Temporal Logic and a Framing Technique for Temporal Logic Programming, PhD thesis, Department of Computing Science, University of Newcastle Upon Tyne, May 1996. Technical report 556
[6] Z Duan, X Yang, M Koutny, Framed temporal logic programming, Science of Computer Programming, 70(1):31-61,2008
[7] Z Duan, M A Koutny, Framed Temporal Logic Programming Language, Journal of Computer Science and Technology, 19(3):341-351,2004.
[8] B Moszkowski, Compositional reasoning about projected and infinite time, In Proceedings of the First IEEE International Conference on Engineering of Complex Computer Systems (ICECCS’95), pages 238–245. IEEE Computer Society Press, 1995
[9] Z Duan, C Tian, L Zhang, A decision procedure for propositional projection temporal logic with infinite models, Acta Informatica, 45(1):43-78, 2008
[10] L Stockmeyer, The Complexity of Decision Problems in Automata Theory and Logic, Ph.D. thesis, MIT,1974
[11] E M Clarke, etc, Model checking, Massachusetts: MIT press, 1999
[12] R Alur, D L Dill, A Theory of Timed Automata, Theoretical Computer Science, 126(2): 183-236, 1994
[13] R Alur, T Feder, T A Henzinger, The benefits of relaxing punctuality, Journal of the ACM, 43(1):116～146, 1996
[14] R Alur, T A Henzinger, A really temporal logic, Journal of the ACM, 41(1):181～204, 1994
[15] C Tian, Z Duan, Model Checking Propositional Projection Temporal Logic Based on SPIN, ICFEM2007, LNCS4789, pp. 246-265, Springer, Heidelberg , 2007
[16] R Alur, T A Henzinger, Logics and models of real time: A survey, Lecture Notes in Computer Science, 600. Springer-Verlag, 74～106, 1992
[17] T Wilke, Specifying timed state sequences in powerful decidable logics and timed automata, Lecture Notes in Computer Science, 863, pp. 694-715, 1994
[18] T A Henzinger, Z Manna, A Pnueli, What good are digital clocks?, In Proc. ICALP’92, volume 623 of LNCS, pages 545–558. Springer, 1992
[19] Z Duan, Modeling of hybrid system, Ph.D thesis, UK: Department of Computer Science, University of Shefield, 1997
[20] Z Duan, Modeling of hybrid systems, Beijing: science press,2004
[21] C Zhou, C A Hoare, A P Ravn, A calculus of durations, Information Processing Letters, 40(5): 269-276, 1991
[22] M Fr?nzle, Model-checking dense-time duration calculus, Formal Aspects of Computing, 16 (2):121-139, 2004
[23] M R Hanson, Model-checking discrete duration calculus, Formal Aspects of Computing, 6A:826-845, 1994.
[24] Z Duan, C Tian, Decidability of Propositional Projection Temporal Logic with Infinite Models, The 4th Annual Conference on Theory and Applications of Models of Computation, shanghai, China, 2007, (NO.377), LNCS, Springer.
[25] C Zhou, M R Hansen, P Sestoft, Decidability and Undecidability Results for Duration Calculus, STACS'93, vol. 665, pp. 58-68, Springer-Verlag, 1993.
[26] G Li, Z Tang, Translating a Continuous-Time Temporal Logic into Timed Automata, Proceedings of the first Asian Symposium on Programming Languages and Systems (APLAS 2003), Lecture Notes in Computer Science 2895, pp.322--338, Springer-Verlag, 2003
[27] L Lamport, The temporal logic of actions, ACM Transactions on programming language and systems,16(3):872-923,1994.
[28] S Demri, P Schnoebelen, The complexity of propositional linear temporal logics in simple cases, Information and Computation, 174(1):84–103, 2002.
[29] C Tian, Z Duan, Propositional Projection Temporal Logic, Büchi Automata and omega-Regular Expressions, in Proceedings, Theory and Applications of Models of Computation, Lecture Notes in Computer Science, 4978, Springer, 2008:47-58.
[30] C Petri, Kommunikation mit Automaten (Communication with Automata), PhD thesis, Technische Universitat Darmstadt, Germany, 1962
[31] M Roger, J Goubault-Larrecq, Log Auditing through Model-Checking, Proceedings of the 14th IEEE workshop on Computer Security Foundations, IEEE Computer Society Washington, DC, USA, 220-234, 2001.
[32] G T Rohrmair, G Lowe, Using data-independence in the analysis of intrusion detection systems, Theoretical Computer Science, 340(1):82-101, 2005.
[33] O Sheyner, J Haines, S Jha, etc, Automated generation and analysis of attack graphs, Proceedings of the 2002 IEEE Symposium on Security and Privacy, 273-284, 2004.
[34] Z Nan, R Mark, P G Dimitar, Evaluating Access Control Policies Through Model Checking, Lecture Notes in Computer Science, Information Security, Springer Berlin, 3650:446-460, 2005.
[35] S Sebastian, V Michael, K Hartmut, Identifying Modeling Errors in Signatures by Model Checking, Lecture Notes in Computer Science, Model Checking Software, Springer Berlin, 5578:205-222, 2009.
[36] J Olivain, J Goubault-Larrecq, The ORCHIDS Intrusion Detection Tool, Proceedings of the 17th International Conference on Computer Aided Verification, Lecture Notes in Computer Science, 3576:286-290, Springer, Edinburgh, Scotland, UK, 2005.
[37] C Tian, Z Duan, Complexity of propositional projection temporal logic with star, Mathematical Structures in Computer Science, 19(1):73-100, 2009
[38] V Goranko, A Montanari, G Sciavicco, A Road Map of Interval Temporal Logics and Duration Calculi, Journal of Applied Non-Classical Logics, 14(1-2): 9-54, 2004
[39] M Hira, D Sarkar, Verification of Tempura Specification of Sequential Circuits, IEEE Trans. on CAD of Integrated Circuits and Systems, 16(4):362-375, 1997.
[40] A Cau, H Zedan, A Coleman, et al, Using ITL and Tempura for Large Scale Specification and Simulation, Proceeding of 4th Euro-micro Workshop on Parallel and Distributed Processing. IEEE Computer Society Press, 493-500,1996
[41] M Solanki, S Tesco, A Framework for Defining Temporal Semantics in Owl Enabled Services, Proceeding of W3C Workshop on Frameworks for Semantics in Web Services. 1-6, 2005.
[42] M Solanki, A Cau, H Zedan, Semantically Annotating Reactive Web Services with Temporal Specifications, Proceedings of the IEEE ICWS 2005, Second International Workshop on Semantic and Dynamic Web Processes. 2005.
[43] Z Duan, L Zhang, A Decision Procedure for Propositional Projection Temporal Logic, Technical Report No.1, Institute of computing Theory and Technology, Xidian University, Xi'an P.R.China, 2005
[44]唐稚松,时序逻辑程序与软件工程,北京:科学出版社,2002。
[45]李广元,唐稚松,带有时钟变量的线性时序逻辑与实时系统验证,软件学报,13(1):33-41,2002
[46]李广元,唐稚松,基于线性时序逻辑的实时系统模型检查,软件学报,13(2):193-202,2002
[47]朱一清,可计算性和计算复杂性,北京:国防工业出版社,2006。
[48]张燕、傅建明、孙晓梅,一种基于模型检查的入侵检测方法,武汉大学学报(理学版),51(3):319-322,2005。
[49] E Clarke, O Grumberg, D Long, Verification Tools for Finite-State Concurrent Systems, A Decade of Concurrency-Reflections and Perspectives, LNCS 803, 124-175, 1993
[50] U Stern, D Dill, A New Scheme for Memory-Efficient Probabilistic Verification. In IFIP TC6/WG6.1 Joint International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols, and Protocol Specification, Testing, and Verification, 333-348, 1996.
[51] P Godefroid, G Holzmann, D Pirottin, State-space caching revisited, Formal Methods in System Design, 7(3):227– 241,1995.
[52] D Peled, Combining Partial Order Reductions with On-the-Fly Model-Checking, Formal Methods in System Design, 8(1):39-64, 1996
[53] D Peled, T Wilke, Stutter-invariant temporal properties are expressible without the next-time operator, Information Processing Letters, 63(5):243-246, 1997
[54] D Dams, O Grumberg, R Gerth, Abstract Interpretation of Reactive Systems. ACM Transactions on Programming Languages and Systems, 19(2), 253-291, 1997
[55] A Sistla, E Clarke, The complexity of propositional linear temporal logics, Journal of the ACM, 32(3):733-749, 1985
[56] P Schnoebelen, The complexity of temporal logic model checking, Proceedings of the 4th. Conference Advances in Modal Logic, vol. 4, pp. 437-459, King's CollegePublication, 2003,
[57] G Holzmann, The model checker SPIN, IEEE Transactions on Software Engineering, 23(5):279-295, 1997
[58] M Vardi, An automata-theoretic approach to linear temporal logic, Proceedings of the VIII Banff Higher order workshop conference on Logics for concurrency : structure versus automata: structure versus automata, 238-266,1996.
[59] A Gurfinkel, O Wei, M Chechik, Systematic Construction of Abstractions for Model-Checking. In 7th Verification, Model Checking, and Abstract Interpretation, LNCS 3855, pages 381–397. Springer-Verlag, 2006.
[60] J Esparza, K Heljanko, A New Unfolding Approach to LTL Model Checking, Lecture Notes in Computer Science, Automata, Languages and Programming, Springer Berlin/Heidelberg, Volume 1853/2000,page 475-486,2000
[61] P Gastin, D Oddoux, Fast LTL to Büchi Automata Translation, Lecture Notes in Computer Science, Computer Aided Verification, Springer Berlin / Heidelberg, Volume 2102/2001,53-65,2001
[62] M Hammer, A Knapp, S Merz, Truly On-the-Fly LTL Model Checking, Lecture Notes in Computer Science, Tools and Algorithms for the Construction and Analysis of Systems, Springer Berlin/Heidelberg, Volume 3440/2005, 191-205, 2005
[63] S Yovine, Model checking timed automata, In Lectures on Embedded Systems, LNCS 1494, pages 114-152. Springer-Verlag, October 1998.
[64] H M Lin, Y Wang, Axiomatising timed automata, Acta Informatica, 38(4): 277–305, 2002.
[65] Markus Muller-Olm, David Schmidt, Bernhard Steffen, Model Checking A Tutorial Introduction. SAS'99, LNCS 1694, pp. 330-354, 1999.
[66] R Gerth, D Peled, M Y Vardi, Simple On-the-fly Automatic Verification of Linear Temporal Logic, In Protocol Specification Testing and Verification, Chapman & Hall, 3-18, 1995.
[67] A He, J Wu, L Li, An Efficient Algorithm for Transforming LTL Formula to Büchi Automaton, 2008 International Conference on Intelligent Computation Technology and Automation (ICICTA), 1215-1219,2008.
[68] C Fritz, Constructing Büchi automata from linear temporal logic using simulation relations for alternating Büchi automata, Proceedings of the 8th international conference on Implementation and application of automata, Lecture Notes In Computer Science, Springer-Verlag, Berlin, Heidelberg, 35-48, 2003.
[69] K Etessami, Temporal massage parlor. http://www1.bell-labs.com/ project/TMP/. 36, 37, 43.
[70] M Daniele, F Giunchiglia, M Vardi, Improved Automata Generation for Linear Temporal Logic, Proceedings of the 11th International Conference on Computer Aided Verification, Lecture Notes In Computer Science, 1633, Springer-Verlag, London, UK, 249 - 260, 1999.
[71] F Somenzi, R Bloem, Efficient Büchi Automata from LTL Formulae, Proceedings of the 12th International Conference on Computer Aided Verification, Lecture Notes In Computer Science, 1855, Springer-Verlag, London, UK, 248,263, 2000.
[72] D Giannakopoulou, F Lerda, Efficient translation of LTL formulae into Büchiautomata, RIACS, Technical Report, 01.29, June 2001.
[73] D Giannakopoulou, F Lerda, From States to Transitions: Improving Translation of LTL Formulae to Büchi Automata, Proceedings of the 22nd IFIP WG 6.1 International Conference Houston on Formal Techniques for Networked and Distributed Systems, Lecture Notes in Computer Science 2529, 308– 326, Springer-Verlag, London, UK, 2002.
[74] M D Wulf, L Doyen, N Maquet, Antichains: Alternative Algorithms for LTL Satisfiability and Model-Checking, Proceedings of TACAS 2008, LNCS 4693, 63-77, Springer-Verlag, Budapest, 2008.
[75] R Bloem, K Ravi, F Somenzi, Efficient decision procedures for model checking of linear time logic properties, In Proceedings of the 11th International Conference on Computer Aided Verification, LNCS 1633, pages 222-235, Springer-Verlag, London, UK,1999.
[76] P Wolper, Constructing Automata from Temporal Logic Formulas : A. Tutorial. Springer Lectures On Formal Methods And Performance Analysis, 261-277, Lectures on formal methods and performance analysis: first EEF/Euro summer school on trends in computer science, Springer-Verlag, New York, 2002.
[77] Ouyang Ming-Guang, Pan Feng, Zhang Yun-Tao, ISITL: Intrusion signatures in augmented interval temporal logic, International Conference on Machine Learning and Cybernetics, v 3, p 1630-1635, 2003
[78] Elzbieta Nowicka, Marcin Zawada, An Interval Temporal Logic-Based Matching Framework for Finding Occurrences of Multi-event Attack Signatures, Computer Network Security, Communications in Computer and Information Science, Volume 1, Part 5, Part 8, 272-285, 2007.
[79] Ouyang Ming-Guang, Zhou Yang-Bo, ISDTM: An intrusion signatures description temporal model, Wuhan University Journal of Natural Sciences, v 8, n 2 A, p 373-378, 2003.
[80] Pratt-Hartmann Ian, Temporal prepositions and their logic, Artificial Intelligence, v 166, n 1-2, p 1-36, 2005.
[81]张琳琳、应时、倪友聪、等,一种软件体系结构关注点分析方法,计算机学报,32(9):1782-1791,2009。
[82] Konur Savas, A decidable temporal logic for events and states, Proceedings of the International Workshop on Temporal Representation and Reasoning, v 2006, p 36-41, 2006.
[83] J R Buchi, On a decision method in restricted second order arithmetic, In Proceedings of the International Congress on Logic, Method, and Philosophy of Science, pages 1-12. Stanford University Press, 1962.
[84] Janicke Helge, Cau Antonio, Siewe Fran?ois, etc, A compositional event & time-based policy model, Seventh IEEE International Workshop on Policies for Distributed Systems and Networks, Policy 2006, IEEE Computer Society, v 2006, p 173-182, 2006.
[85] Pandya, K Paritosh, The saga of synchronous bus arbiter: On model checking quantitative timing properties of synchronous programs, Electronic Notes in Theoretical Computer Science, v 65, n 5, p 894-908, July 2002.
[86] Kazhamiakin Raman, Pandya Paritosh, Pistore Marco, Timed modelling and analysis in Web service compositions, First International Conference on Availability, Reliability and Security, ARES 2006, IEEE Computer Society, v 2006, p 840-846, 2006.
[87] Kazhamiakin Raman, Pandya Paritosh, Pistore Marco, Representation, verification, and computation of timed properties in Web service compositions, IEEE International Conference on Web Services, IEEE Computer Society, p 497-504, 2006.
[88] Ruggero Lanotte, Andrea Maggiolo-Schettini, Simone Tini, Concurrency in timed automata, Theoretical Computer Science, 309(1-3): 503-527, 2003.
[89]张海宾、段振华,区间时序逻辑的模型检查,西安电子科技大学学报(自然科学版),36(2):338-342,2009
[90]张海宾、段振华,稠密时间区间时序逻辑的可满足性判定,西安电子科技大学学报(自然科学版),34(3):463-467,2009
[91]裴玉、徐启文、李宣东、等, QRDChecker:一个QRDC模型检验工具,软件学报,16(3):355-364,2005
[92]张海宾、段振华,多速率混合系统的模型检查,西安电子科技大学学报(自然科学版),35(1):60-64、86,2008
[93] H Ma, L Li, W Wang, etc, Automatic synthesis of the DC specifications of lip synchronisation protocol, Proceedings of the Asia-Pacific Software Engineering Conference and International Computer Science Conference, APSEC and ICSC, p 371-378, IEEE Computer Society, 2001.
[94]雷丽晖、段振华,使用扩展区间时序逻辑为并发工作流建模,西安电子科技大学学报(自然科学版),34(4):673-680,2007
[95] L Zhang, Combining formal specification methods and informal specification methods for requirement analysis, IEEE Pacific RIM Conference on Communications, Computers, and Signal Processing - Proceedings, v 1, p 444-447, 1997.
[96] B Moszkowski, Using temporal logic to analyse temporal logic: A hierarchical approach based on intervals, Journal of Logic and Computation, v 17, n 2, p 333-409, 2007.
[97] Pratt-Hartmann Ian, Temporal prepositions and their logic: Extended abstract, Proceedings of the International Workshop on Temporal Representation and Reasoning, v 11, p 7-8, 2004.
[98] B Dines(著),刘伯超(译),软件工程,北京:清华大学出版社,2010
[99] Bowman Howard, Faconti Giorgio, Analysing cognitive behaviour using LOTOS and Mexitl, Formal Aspects of Computing, v 11, n 2, p 132-159, 1999.
[100]王小兵、段振华,面向投影时序逻辑的Web服务模型检测,西安交通大学学报,43(4):39-43、124,2009。
[101]雷丽晖、段振华,基于扩展投影时序逻辑的组合Web服务描述与验证,西安交通大学学报,41(10):1155-1159,2007。
[102]舒新峰、段振华,利用投影时序逻辑的多内核进程调度建模与验证,西安交通大学学报,44(33):52-57,2010。
[103]舒新峰、段振华,投影时序逻辑的公理系统与形式验证,西安电子科技大学学报(自然科学版),36(4):680-685、729,2009。
[104]王小兵、段振华,框架投影时序逻辑程序设计语言中的指针,西安电子科技大学学报(自然科学版),35(6):1069-1074,2008。
[105]杨琛、段振华、王小兵,面向命题投影时序逻辑的安全协议模型检测,西安交通大学学报,44(8):30-35,2010。
[106] Z Duan, N Zhang, A complete axiomatization of Propositional Projection Temporal Logic, Proceedings - 2nd IFIP/IEEE International Symposium on Theoretical Aspects of Software Engineering, TASE 2008, p 271-278, 2008.
[107] Z Duan, C Tian, A unified model checking approach with projection temporal logic, Lecture Notes in Computer Science, v 5256 LNCS, p 167-186, 10th International Conference on Formal Engineering Methods, ICFEM 2008, Oct 27– 31, Verlag, 2008.
[108]王小兵、段振华,面向对象的时序逻辑语言,电子科技大学学报,38(1):97-101、107,2009。
[109] P Zhang, Z Duan, C Tian, UML statecharts' PTL formal semantics, 3rd International Symposium on Intelligent Information Technology Application, IITA 2009, v 1, p 381-385, IEEE Computer Society, 2009.
[110] Z Duan, X Yang, K Maciej, Semantics of framed temporal logic programs, Lecture Notes in Computer Science, 21st International Conference on Logic Programming, Springer Verlag, v 3668, p 356-370, 2005.
[111]张海宾,、段振华,混合系统的符号化可达性分析,软件学报,19(12):3111-3121,2008。
[112] H Zhang, Z Duan, Symbolic Algorithmic Analysis of Rectangular Hybrid Systems, Journal of Computer Science and Technology, 24(3):534-543, 2009.
[113]张海宾,、段振华,多速率混合系统的符号化可达性分析,西安交通大学学报,41(4):412-415,2007。
[114] C Tian, Z Duan, A note on stutter-invariant PLTL, Information Processing Letters, 109(13):663-667, 2009.
[115]王小兵,面向对象MSVL语言及其在组合Web服务验证中的应用,博士学位论文,西安:西安电子科技大学计算机学院,2009。
[116] X Yang, Formal Semantics of Framed Temporal Logic Programming Language MSVL, Ph.D thesis, Xi’an: School of Computer Science, Xidian University, P R China, 2009.
[117] H Zhang, Formal Verification of Hybrid Systems, Ph.D thesis, Xi’an: School of Computer Science, Xidian University, P R China, 2007.
[118] Z Duan, C Yang, Unconditional secure communication: a Russian Cards protocol, Journal of Combinatorial Optimization, 19(4): 501-530, 2010.
[119] Christel Baier,Joost-Pieter Katoen,Principles of Model Checking,The MIT Press,Cambridge, Massachusetts,London, England,2004
[120] Rodolfo Gomez, Howard Bowman, A MONA-based Decision Procedure for Propositional Interval Temporal Logic, Workshop of Interval Temporal Logics and Duration Calculi (part of the 15th European Summer School in Logic, Language and Information, August 2003. http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.2.3812&rep=rep1&type=pdf
[121]晏荣杰、李广元、徐雨波、等,有限精度时间自动机的可达性检测,软件学报,17(1):1-10,2006。
[122] Patricia Bouyer, Nicolas Markey, Jo?l Ouaknine, etc, On Expressiveness and Complexity in Real-time Model Checking, Proceedings of the 35th international colloquium on Automata Languages and Programming, Part II, 2008. http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.151.2670&rep=rep1&type=pdf
[123] Jo?l Ouaknine, Alexander Rabinovich, James Worrell, Time-Bounded Verification, Proceedings of CONCUR 09 (improved and expanded version), LNCS 5710, 19 pages, 2009. http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.153.6937&rep=rep1&type=pdf
[124] Dang Van Hung, Phan Hong Giang, A Sampling Semantics of Duration Calculus, Formal Techniques for Real-Time and Fault Tolerant Systems, LNCS 1135, Spriger-Verlag, 1996. http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.103.6577&rep=rep1&type=pdf
[125] Martin Franzle, Michael R Hansen, Efficient Model Checking for Duration Calculus, International Journal of Software Informatics, 3(2-3):171-196, 2009.
[126] V A Braberman, D V Hung, On Checking Timed Automata for Linear Duration Invariants, Proceedings of 19th the IEEE Real-Time Systems Symposium, 1998. http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.12.7174&rep=rep1&type=pdf
[127] Pham Hong Thai, Dang Van Hung, Verifying Linear Duration Constraints of Timed Automata, Theoretical Aspects of Computing - ICTAC 2004, Lecture Notes in Computer Science, Volume 3407/2005, 295-309, SPRINGER-VERLAG, Germany, 2005.
[128] D'Silva Vijay, Kroening Daniel,Weissenbacher Georg, A Survey of Automated Techniques for Formal Software Verification, IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 27(7): 1165-1178, 2008.
[129] Dennis Dams, Abstraction in Software Model Checking: Principles and Practice, Model checking software: 9th International SPIN Workshop, Vol 2318: 14-22, LNCS, Springer-Verlag, 2002.
[130] T Paul Darga, Chandrasekhar Boyapati, Efficient Software Model Checking of Data Structure Properties, Proceedings of the 21st annual ACM SIGPLAN conference on Object-oriented programming systems, languages, and applications, Volume 41 Issue 10, 363-382, October 2006
[131] Tevfik Bultan, Aysu Betin-Can, Scalable Software Model Checking Using Design for Verification, In Proceedings of the IFIP Working Conference on Verified Software: Theories, Tools, Experiments, Lecture Notes in Computer Science, Volume 4171/2008, 337-346, 2008.
[132] V Shobha, A Jacob. Abraham, Static program transformations for efficient software model checking, IFIP International Federation for Information Processing, Volume 156/2004, Building the Information Society, 257-281, 2004.
[133] Radu Iosif , Symmetry Reduction Criteria for Software Model Checking, Proceedings of the 9th International SPIN Workshop on Model Checking of Software, 22– 41, Springer-Verlag London, UK, 2002.
[134] Patrice Godefroid, Software model checking: the verisoft approach, Formal Methods in System Design, Volume 26, Number 2, 77-101, 2005.
[135] Patrice Godefroid, Software Model Checking Improving Security of a Billion Computers, Proceedings of the 16th International SPIN Workshop on Model Checking Software, Lecture Notes in Computer Science, Volume 5578/2009, 1-1, 2009.
[136]并发实时系统的理论与方法, http://lcs.ios.ac.cn/introduce/concurrency.htm, 2006.
[137]吴尽昭、王永祥、覃广平,交互式马尔可夫链——并发系统的设计、验证与评价(数学机械化丛书),北京:科学出版社,2007。
[138] Howard Bowman, Helen Cameron, Peter King, Mexitl: Multimedia in Executable Interval Temporal Logic, Formal Methods in System Design, Volume 22, Number 1, 5-38, 2003.
[139] Rodolfo Gómez, Howard Bowman, PITL2MONA: Implementing a Decision Procedure for Propositional Interval Temporal Logic, Journal of Applied Non-Classical Logics , Volume 14, Number 1-2, 105-148, 2004.
[140] James Glenn, William Gasarch, Implementing WS1S via Finite Automata, the First International Workshop on Implementing Automata, Lecture Notes in Computer Science, Volume 1260/1997, 50-63, 1997.
[141] E Asarin, P Caspi, O Maler, A Kleene theorem for timed automata, Proceedings of the 12th Annual IEEE Symposium on Logic in Computer Science, p.160-171, Warsaw , Poland, 1997.
[142] Eugene Asarin, Paul Caspi, Oded Maler, Timed Regular Expressions, Journal of the ACM, Volume 49 Issue 2, 172-206, 2002.
[143] Lange Martin, Temporal Logics for Non-Regular Properties Model Checking, Proc.\ 4th Int.\ Workshop on Methods for Modalities, HU Berlin, Berlin, Germany, 194:1-7, 2005.
[144] Julian Bradfield, Colin Stirling, Modal Mu-Calculi, Handbook of Modal Logic, Elsevier, 721-756, 2007. http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.143.9834&rep=rep1&type=pdf
[145] E Emerson, Model Checking and the Mu-calculus, Descriptive Complexity and Finite Models, American Mathematical Society, pp. 185–214, 1996. http://www.cs.utexas.edu/users/emerson/Pubs/1996-01.Em.mod-chk-and-mu-calc.ps
[146]林惠民、张文辉,模型检测:理论、方法与应用,电子学报,30(12A):1907-1912,2002。
[147] Slawomir Lasota, Igor Walukiewicz, Alternating timed automata, ACM Transactions on Computational Logic, 9(2): 1–26, 2008.
[148] Deepak D’Souza, M Raj Mohan, Eventual Timed Automata, In Foundations of Software Technology and Theoretical Computer Science, Lecture Notes in Computer Science, Volume 3821, 322-334, 2005
[149] B C Moszkowski, A complete axiomatization of interval temporal logic with infinite time, In. Proc. 15th Annual IEEE Symp. on Logic in Computer Science, 241-252, IEEE Computer Society Washington, DC, USA, 2002.
[150] B C Moszkowski, An automata-theoretic completeness proof for interval temporal logic, Proceedings of the 27th International Colloquium on Automata, Languages and Programming, 223-234, Springer-Verlag London, UK, 2000.
[151] B C Moszkowski, Compositional reasoning using interval temporal logic and tempura, International Symposium on Compositionality: The Significant Difference, Lecture Notes in Computer Science, Volume 1536, 439-464, 1998.
[152] A Cau, B Moszkowski, Using PVS for interval temporal logic proofs. Part 1: The syntactic and semantic encoding, Technical Monograph 14, SERCentre, De Montfort University, Leicester, 1996.
[153] A Zinoviev, ITL as a Language for Regular Relations, In: Proceedings of 4th Panhellenic. Loguc Symposium, 2003. http://www2.cs.ucy.ac.cy/projects/pls4/Zinoviev.ps
[154] D P Guelev, Van Hung, Prefix and projection onto state in duration calculus, Electronic Notes in Theoretical Computer Science, vol. 65, Elsevier Science Publishers, Amsterdam, 2002.
[155] He Jifeng, A Behavioral Model for Co-design, Proceedings of the Wold Congress on Formal Methods in the Development of Computing Systems-Volume II, p.1420-1438, September 20-24, 1999.
[156] Dang Van Hung, Projections: A Technique for Verifying Real-Time Programs in Duration Calculus. Technical Report 178, UNU-IIST, P.O. Box 3058, Macau, November 1999. Published in the proceedings of the Conference on Information Technology and Education, Ho Chi Minh City, Vietnam, January 2000.
[157] S Kono, A Combination of Clausal and Non Clausal Temporal Logic Program, IJCAI-93 Workshop on Executable Modal and Temporal Logics, Lecture Notes in Computer Science, Volume 897, 69-85, 1995.
[158] Howard Bowman, Simon Thompson, A tableau method for interval temporal logic, Technical report. University of Kent at Canterbury, 1997.
[159] Z Manna, A Pneuli, Verification of Concurrent Programs: The Temporal Framework, The Correctness Problem in Computer Science (R. S. Boyer and J. S. Moore, eds.), International Lecture Series in Computer Science, 1981. Also in Annals of Pure and Applied Logic, Volume 51, Issues 1-2, Pages 79-98, 1991.
[160] Akio Nakata, Teruo Higashino, Deriving parameter conditions for periodic timed automata satisfying real-time temporal logic formulas, 21st International Conference on Formal Techniques for Networked and Distributed Systems, 151-168, Kluwer, B.V. Deventer, The Netherlands, The Netherlands, 2001.
[161] Ahmed Bouajjani, Yassine Lakhnech, Sergio Yovine, Model checking for extended timed temporal logics, Proceedings of the 4th International Symposium onFormal Techniques in Real-Time and Fault-Tolerant Systems, 306-326, Springer-Verlag London, UK, 1996.
[162] Ahmed Bouajjani, Yassine Lakhnech, Temporal logic + timed automata: expressiveness and decidability, Proceedings of the 6th International Conference on Concurrency Theory, 531-545, Springer-Verlag London, UK, 1995.
[163] Z Duan, M Holcombe, Timed interval temporal logic and modelling of hybrid systems, in Proceedings of Modelling and Simulation ESM'94, Barcelona, Spain, June 1-3, pp. 534-41, 1994.
[164] Deutsche Forschungsgemeinschaft, Forderkennzeichen La, Martin Fr?nzle, Decidability of duration calculi on restricted model calsses, http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.12.105&rep=rep1&type=pdf, 1996.
[165] C Zhou, D V Hung, X Li, A duration calculus with infinite intervals, Proceedings of the 10th International Symposium on Fundamentals of Computation Theory, Lecture Notes in Computer Science, Volume 965, 16-41, 1995.
[166] C A R Hoare, Communicating sequential processes, Prentice Hall International Series in Computing Science, Prentice Hall, 1985. Also in http://www.usingcsp.com/cspbook.pdf
[167] G M Reed, A W Roscoe, A timed model for communicating sequential processes, Theoretical Computer Science, Volume 58 Issue 1-3, 249-261, 1988.
[168] Dan R Ghica, A games-based foundation for compositional software model checking, Ph.D thesis, Queen’s University, Kingston, Ontario, Canada, 2002.
[169]武新华,黑客命令与典型应用,北京:中国铁道出版社,2009。
[170] Glynn Winskel(著),宋国新、邵志清(译),程序设计语言的形式语义,北京:机械工业出版社,2004。
[171]王永祥、吴尽昭、蒋建民,进程代数---对称与动作细化,数学机械化丛书,北京:科学出版社,2007。
[172]古天龙,软件开发的形式化方法,北京:高等教育出版社,2005。
[173] J邦詹森、G古廷(著),姚兵、张忠辅(译),有向图的理论、算法及其应用,北京:科学出版社,2009。
[174] T A Henzinger, The Temporal Specification and Verification of Real-Time Systems, PhD thesis, Stanford University, August 1991.
[175] Joost-Pieter Katoen, Concepts, algorithms and tools for model checking, 1999. http://www.cs.aau.dk/~kgl/VERIFICATION99/katoen2.ps
[176] L Gonnord, N Halbwachs, P Raymond, From discrete duration calculus to symbolic automata, In 3rd International Workshop on Synchronous Languages, Applications, and Programs, SLAP’04, Barcelona, Spain, March 2004. Also in Electronic Notes in Theoretical Computer Science (ENTCS), Volume 153 Issue 4, 3-18, June, 2006.
[177] F Pieniazek, V Braberman, On Checking Finitary Timed Automata for Duration Properties, Tech. Rep. UBA, TR99-007, 1999. http://www.dc.uba.ar/people/proyinv/tr.html
[178] Alexander Rabinovich, On expressive completeness of duration and mean value calculi, Theoretical Computer Science, Volume 230 Issue 1-2, 2000.http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.38.5393&rep=rep1&type=ps
[179] X Li, Decidability of Mean Value Calculus, Journal of Computer Science and Technology, 14(2): 173-180, 1999.
[180] Ben Moszkowski, Benefits of Interval Temporal Logic for Specification of Concurrent Systems, http://www.cl.cam.ac.uk/~md466/ccw2010/moszkowski-temporal.pdf, 2010.
[181] Z Duan, M Holcombe, A hybrid projection temporal logic for hybrid systems, http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.54.9022&rep=rep1&type=pdf, 1998.
[182] Michael Reichhardt Hansen, Dang Van Hung, A Theory of Duration Calculus with Application, Domain Modeling and the Duration Calculus, Lecture Notes in Computer Science, Volume 4710, 119-176, 2007.
[183] Y LI, D V Hung, Checking temporal duration properties of timed automata, Journal of Computer Science and Technology, Volume 17 Issue 6, 689-698, November 2002.
[184] Michael R Hansen and Zhou Chaochen, Duration calculus logical foundations, Formal Aspects of Computing, Volume 9, Number 3, 283-330, 1997.
[185] D Guelev, Logical Interpolation and Projection onto State in the Duration Calculus, Journal of Applied Non-classical Logics, 14(1-2): 181-208, 2004.
[186] Roland Meyer, Johannes Faber, Andrey Rybalchenko, Model checking Duration Calculus a practical approach, Formal Aspects of Computing, Volume 20 Issue 4-5, 332-346, June 2008.
[187] Dimitar P Guelev, Dang Van Hung, On the completeness and decidability of duration calculus with iteration, Theoretical Computer Science, 337(1-3): 278-304, 2005.
[188] D V Hung, J Wang, On the design of hybrid control systems using automata models, Proceedings of the 16th Conference on Foundations of Software Technology and Theoretical Computer Science, Lecture Notes in Computer Science, Volume 1180, 156-167, 1996.
[189]侯建民、李宣东、郑国梁,离散时段演算的符号模型验证,计算机学报,21(2):103-110,1998。
© 2004-2018 中国地质图书馆版权所有 京ICP备05064691号 京公网安备11010802017129号 地址：北京市海淀区学院路29号 邮编：100083 电话：办公室：(+86 10)66554848；文献借阅、咨询服务、科技查新：66554700 |