Matthew B. Dwyer
George S. Avrunin
James C. Corbett
- 1.G. Avrunin, U. Buy, J. Corbett, L. Dillon, and J. Wileden. Automated analysis of concurrent systems with the constrained expression toolset. IEEE Transactions on Software Engineering, 17(11):1204-1222, Nov. 1991. Google Scholar
Digital Library
- 2.K. M. Chandy and J. Misra. Parallel Program Design: A Foundation. Addison Wesley Publishing Company, Inc., Reading, Massachusetts, 1988. Google ScholarDigital Library
- 3.E. Clarke, E. Emerson, and A. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems, 8(2):244-263, Apr. 1986. Google ScholarDigital Library
- 4.R. Cleaveland, J. Parrow, and B. Steffen. The Concurrency Workbench: A semantics based tool for the verification of concurrent systems. ACM Transactions on Programming Languages and Systems, 15(1):36-72, Jan. 1993. Google ScholarDigital Library
- 5.J. C. Corbett and G. S. Avrunin. Using integer programming to verify general safety and liveness properties. Formal Methods in System Design, 6:97-123, Jan. 1995. Google ScholarDigital Library
- 6.R. Darimont and A. van Lamsweerde. Formal refinement patterns for goal-driven requirements elaboration. In D. Garlan, editor, Proceedings of the Fourth ACM SIGSOFT Symposium on the Foundations of Software Engineering, pages 179-190, San Francisco, Oct. 1996. ACM (Proceedings appeared in Software Engineering Notes, 21(6). Google ScholarDigital Library
- 7.L. K. Dillon, G. Kutty, L. E. Moser, P. M. Melliar- Smith, and Y. S. Ramakrishna. A graphical interval logic for specifying concurrent systems. ACM Transactions on Software Engineering and Methodology, 3(2):131-165, Apr. 1994. Google ScholarDigital Library
- 8.Dover, G. Avrunin, and J. Corbett. A System of Specification Patterns. http: //uvw . cis . ksu. edu/ santos/spec-patterns, 1997.Google Scholar
- 9.M. Dwyer, G. Avrunin, and J. Corbett. Property specification patterns for finite-state verification. In M. Ardis, editor, Proceedings of the Second Workshop on Formal Methods in Software Practice, pages 7-15, Mar. 1998. Google ScholarDigital Library
- 10.M. Dwyer and L. Clarke. Data flow analysis for verifying properties of concurrent programs. Software Engineering Notes, 19(5):62-75, Dec. 1994. Proceedings of the Second ACM SIGSOFT Symposium on Foundations of Software Engineering. Google ScholarDigital Library
- 11.N. E. Fuchs 'and R. Schwitter. Attempt0 Controlled English (ACE). In CLAW 96, the First International Workshop on Controlled Language Applications, 1996.Google Scholar
- 12.E. Gamma, R. Helm, R. Johnson, and J. Vlissides. Design Patterns: Elements of Reusable Object-Oriented Software. Addison-Wesley, 1994. Google ScholarDigital Library
- 13.N. Halbwachs, P. Caspi, P. Raymond, and D. Pilaud. The synchronous programming language LUS- TRE. Proceedings of the IEEE, 79(9), Sept. 1991.Google ScholarCross Ref
- 14.Z. Har'El and R. P. Kurshan. Software for analytical devleopment of communication protocols. AT&T Technical Journal, 69(1):44-59, 1990.Google Scholar
- 15.L. Lamport. The Temporal Logic of Actions. ACM Transactions on Programming Languages and Systems, 16(3):872-923, May 1994. Google ScholarDigital Library
- 16.Z. Manna and A. Pnueli. Tools and rules for the practicing verifier. Technical Report STAN-CS-90-1321, Stanford University, July 1990. appeared in Carnegie Mellon Computer Science: A 25 year Commemorative, ACM Press, 1990. Google ScholarDigital Library
- 17.Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer- Verlag, 1991. Google ScholarDigital Library
- 18.P. Massonet and A. van Lamsweerde. Analogical reuse of requirements frameworks. In Proceedings of RE '97- Third International Conference on Requirements Engineering, 1997. Google ScholarDigital Library
- 19.K. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993. Google ScholarDigital Library
- 20.K. Olender and L. Osterweil. Cecil:, A sequencing constraint language for automatic static analysis generation. IEEE nansuctions on Software Engineering, 16(3):268-280, Mar. 1990. Google ScholarDigital Library
- 21.S. S. Owicki and L. Lamport. Proving liveness properties of concurrent systems. ACM 'i'+ansactions on Programming Languages and Systems, 4:455495, July 1982. Google ScholarDigital Library
- 22.D. Rosenblum. Formal methods and testing: Why the state-of-the-art is not the state-of-the-practice (IS- STA'96/FMSP'96 panel summary). ACM SIGSOFT Software Engineering Notes, 21(4), July 1996. Google ScholarDigital Library
Index Terms
- Patterns in property specifications for finite-state verification
Recommendations
Property specification patterns for finite-state verification
FMSP '98: Proceedings of the second workshop on Formal methods in software practiceManaging space for finite-state verification
ICSE '06: Proceedings of the 28th international conference on Software engineeringFinite-state verification (FSV) techniques attempt to prove properties about a model of a system by examining all possible behaviors of that model. This approach suffers from the state-explosion problem, where the size of the model or the analysis costs ...
Patterns for Timed Property Specifications
Patterns for property specification enable non-experts to write formal specifications that can be used for automatic model checking. The existing patterns identified in [Dwyer, M.B., G.S. Avrunin and J.C. Corbett, Property specification patterns for ...
Comments