- 1.Bartlett, K.A., Scantlebury, R.A., and Wilkinson, P.T. "A note on reliable full-duplex transmission over halfduplex lines," Comm. of the ACM, Vol. 12, No. 5, (1969), pp. 260-265. Google ScholarDigital Library
- 2.Bellcore LSSGR, LATA Switching Systems Generic Requirements, FR-NWT-000064, 1992. Incl: SPCS Capabilities and Features, SR-504: 1, (March 1996).Google Scholar
- 3.LSSGR, FSD 01-02-1450, p. 8.Google Scholar
- 4.LSSGR, FSD 01-02-1201, p. 2.Google Scholar
- 5.Buchi, J.R., "On a decision method in restricted secondorder arithmetics," Proc. 1960 Int. Cong. on Logic, Methods, and Philosophy of Science, Stanford University Press, (1962), pp. 1-12.Google Scholar
- 6.Ghan, W., Anderson, R.J., Beame, P., et al., "'Model checking large software specifications," IEEE Trans. on Software Engineering, Vol. 24, No. 7, (1998), pp. 498- 519. Google ScholarDigital Library
- 7.Chaves, J.A., "Formal Methods at AT&T - An Industrial Usage Report," Proc. 4th Conf on Formal Description Techniques, North-Holland, Amsterdam, (1992), pp. 83- 90. Google ScholarDigital Library
- 8.Colby, C., Godefroid, P., Jagadeesan, L., "Automatically closing open reactive programs," Proc. ACM SIGPLAN Conf on Programming Language Design and Implementation, Montreal, (June 1998), pp. 345-357. Google ScholarDigital Library
- 9.Dwyer, M.B ., Avrunin, G.S., Corbett, J.C., "Property Specification Patterns for Finite-state Verification," Proc. 2nd Workshop on Formal Methods in Software Practice, Ft. Lauderdale, (March 1998). Google ScholarDigital Library
- 10.Gerth, R., Peled, D., Vardi, M.Y., Wolper, P., "Simple On-the-fly Automatic Verification of Linear Temporal Logic," Proc. Conf on Protocol Specification, Testing and Verification, Warsaw, Poland. Chapman & Hall, Germany, (1995), pp. 173-- 184. Google ScholarDigital Library
- 11.Godefroid, P., "VeriSoft: A Tool for the Automatic Analysis of Concurrent Reactive Software," Proc. 9th Conf on Computer Aided Verification, Haifa, (June 1997). LNCS 1254, pp. 476-479, Springer-Verlag. Google ScholarDigital Library
- 12.Hoare, C.A.R., "Communicating sequential processes," Comm. of the ACM, Vol. 21, No. 8, (1978), pp. 666-677. Google ScholarDigital Library
- 13.Holzmann, G.J., "The Theory and Practice of a Formal Method: NewCoRe," Proc. ZFIP World Computer Congress, Vol. I, Hamburg, Germany, (August 1994), pp. 35- 44 North-Holland Publ.Google Scholar
- 14.Holzmann, G.J., "The model checker SPIN," IEEE Trans. on SofhYare Engineering, Vol. 23, No. 5, (1997), pp. 279-295. Google ScholarDigital Library
- 15.Marick, B., The Craft of Software Testing, Prentice Hall, (1995), Englewood Cliffs, NJ, USA.Google Scholar
- 16.Pnueli, A., "The temporal logic of programs," Proc. 18th IEEE Symposium on Foundations of Computer Science, Providence, R.I.,.(1977), pp. 46-57.Google Scholar
- 17.Saracco, R., Smith, J.R.W., Reed, R., Telecommunications Systems Engineering using SDL, North-Holland Publ, (1989), 632 pgs. Google ScholarDigital Library
Index Terms
A practical method for verifying event-driven software
Recommendations
An Automated Verification Method for Distributed Systems Software Based on Model Extraction
Software verification methods are used only sparingly in industrial software development today. The most successful methods are based on the use of model checking. There are, however, many hurdles to overcome before the use of model checking tools can ...
The software model checker Blast: Applications to software engineering
Blast is an automatic verification tool for checking temporal safety properties of C programs. Given a C program and a temporal safety property, Blast either statically proves that the program satisfies the safety property, or provides an execution path ...
Bounded model checking of high-integrity software
HILT '13: Proceedings of the 2013 ACM SIGAda annual conference on High integrity language technologyModel checking [5] is an automated algorithmic technique for exhaustive verification of systems, described as finite state machines, against temporal logic [9] specifications. It has been used successfully to verify hardware at an industrial scale [6]. ...
Comments