An industrial application of symbolic model checking
Tóm tắt
Từ khóa
Tài liệu tham khảo
Bäumler S, Balser M, Dunets A, Reif W, Schmitt J (2006) Verification of Medical Guidelines by Model Checking – A Case Study http://spinroot.com/spin/Workshops/ws06/027.pdf
Bundesamt für Sicherheit in der Informationsgesellschaft (BSI) (2005) Common Criteria for Information Technology Security Evaluation, Part 3. http://www.bsi.de/cc/ccpart3v2_3.pdf
Burch JR, Clarke EM, Long DE (1994) Symbolic Model Checking for Sequential Circuit Verification. IEEE Trans Comp Aided Design Integr Circ Syst 13:401–424
Chan W, Anderson RJ, Beame P, Burns S, Modugno F, Notkin D, Reese JD (1998) Model checking large software specifications. IEEE Trans Softw Eng 24(7):498–520
Cimatti A, Clarke EM, Giunchiglia F, Roveri M (2000) NuSMV: a new symbolic model verifier. In: Halbwachs N, Peled D (eds) International Conference on Computer-Aided Verification (CAV’99), LNCS, vol 1633, pp 495–499, Springer, Berlin Heidelberg
Cimatti A (2000). Industrial Applications of Model Checking. In: Cassez F, Jard C, Rozoy B, Ryan MD (eds.) Modeling and Verification of Parallel Processes (MOVEP’00), LNCS, vol. 2067, pp 153–167, Springer, Berlin Heidelberg
Clarke EM, Grumberg O, Peled DA (1999) Model Checking. The MIT Press, Cambridge, MA, USA
Helke S, Kammüller F (2005) Property Preserving Abstraction for Statecharts. In: 25th IFIP WG 6.1 International Conference on Formal Techniques for Networked and Distributed Systems, FORTE 2005, LNCS, vol. 3731, pp 305–319, Springer, Berlin Heidelberg
Holzmann GJ (1991) Design and Verification of Computer Protocols. Prentice Hall, London
Janssen W, Mateescu R, Mauw S, Fennema P, van der Stappen P (1999) Model checking for managers. In: Proceedings Theoretical and Practical Aspects of SPIN Model Checking, LNCS, vol 1680, pp 92–107, Springer, Berlin Heidelberg
Lamport L (1994) The temporal logic of actions. ACM Trans Prog Lang Syst 16:872–923 http://doi.acm.org/10.1145/177492.177726
Larsen K G, Steffen B, Weise C (1997) Continuous Modelling of Real Time and Hybrid Systems: From Concepts to Tools. Int J Softw Tools Technol Transf 1:64–85
Manna Z, Pnueli A (1991) The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag, New York
McMillan KL (1992) Symbolic Model Checking – an Approach to the State Explosion Problem. School of Computer Science, Pittsburgh PA, Carnegie Mellon University
McMillan KL (1995) Symbolic Model Checking. Kluwer Academic Publishers, Norwell, MA, USA
nuSMV (1999) NuSMV examples: the collection. http://nusmv.irst.itc.it/examples/examples.html
Preibusch S (2006) http://preibusch.de/projects/TWIN/
ThyssenKrupp (2005) Safe distance – Four-level safety concept. http://twin-elevator.com/Safe_distance.353.0.html?L=1
ThyssenKrupp (2005) Higher performance. http://twin-elevator.com/New_buildings.368.0.html?L=1
Uppsala University, Department of Information Technology (2006) UPPAAL. http://www.uppaal.com/