This page contains links to papers. To save space, postscript/pdf.gz files have compressed with gzip. Use gunzip (Unix/linux) or WinZip (PC) to uncompress the files.

• VISUALIZING VERIFICATION
  
  
  • Marsh A., Visualizing Verification ( pdf.gz ), Scholarly Paper, Master of Science in Systems Engineering, University of Maryland, College Park, April 2004.

• VALIDATION/VERIFICATION OF QUEUEING SYSTEMS
  
  
  • Kleijnen J., Verification and Validation of Simulation Models ( pdf.gz ), European Journal of Operational Research, Vol. 82, 1995, pp. 145-162.
  • Osman Balci and Robert G. Sargent, Some Examples of Simulation Model Validation Using Hypothesis Testing ( pdf.gz )..... Virginia Polytechnic Institute & State University and Syracuse University, 1982.
  • Takayuki Osogami, Adam Wierman, Mor Harchol-Balter, and Alan Scheller-Wolf, How many servers are best in a dual-priority FCFS system? ( pdf.gz )..... Technical Report: CMU-CS-03-201, School of Computer Science, Carnegie Mellon University, Pittsburgh, PA 15213, November 2003

• CONSTRAINT-BASED APPROACHES TO VALIDATION
  
  
  • Waters R.C., System Validation via Constraint Modeling ( pdf.gz ), ACM SIGPLAN Notics, Volume 26, No. 8, August 1991.

• SPECIFICATION-BASED TESTING
  
  
  • Jagadeesan L.J., et al, Specification-Based Testing of Reactive Software: A Case Study in Technology Transfer ( ps.gz ), February, 1997.
  • Jagadeesan L.J., et al, Specification-Based Testing of Reactive Software: Tools and Experiments ( ps.gz ), Proceedings of the International Conference on Software Engineering, May 1997.
  • Alexander R.T., Blackburn M., Component Assesment using Specification-Based Analysis and Testing ( pdf.gz ), SPC-98095-CMC, Software Productivity Consortium, Herndon, VA 20170, May 1999.
  • Burton S., Automated Generation of High Integrity Test Suites from Graphical Specifications ( pdf.gz ), Ph.D. Thesis, Department of Computer Science, University of York, March 2002.
  • Bergner K. et al, A Formally Founded Componentware Testing Methodology ( pdf.gz ), Institut for Informatik, Munich, Germany, April 2001.
  • Vieira M.E., Dias M.S., Richardson D.J., Object-Oriented Specification-Based Testing Using UML Statechart Diagrams , ( pdf.gz ), ICSE 2000, Limerick, Ireland, 2000.

• SPECIFICATION-BASED TESTING WITH LTSA
  
  
  • Stooper P. Specification-Based Testing of Concurrent Programs ( pdf.gz ), Bachelor of Information Technology Thesis, University of Queensland, Australia, October 2002.
  • Magee J., et al, Graphical Animation of Behavior Models ( pdf.gz ), ICSE 2000, Limerick, Ireland, 2000.
  • Uchitel S., Kramar J., Magee J., Incremental Elaboration of Scenario-Based Specifications and Behavior Models using Implied Scenarios ( pdf.gz ), ACM Transactions on Software Engineering and Methodology, Volume 13, No. 1, January 2004, Pages 37-85.
  • Uchitel S. and Yankelevich D., Enhancing Architectural Mismatch Detection with Assumptions ( pdf.gz ). (This paper presents two problems: a system for tracking trucks in freight transportation, and behavior of a gas station.)

• CLASSICAL LOGIC
  
  
  • Gertz M., Introduction to Logic ( pdf.gz ), Class Notes from ECS 289G, Logics and Knowledge Representation, University of California, Davis, January 2002.
  • Gertz M., Propositional Logic (Review) ( pdf.gz ), Class Notes from ECS 289G, Logics and Knowledge Representation, University of California, Davis, January 2002.
  • Gertz M., First-Order Logic ( pdf.gz ), Class Notes from ECS 289G, Logics and Knowledge Representation,
  • Galton A., Logic as a Formal Method ( ps.gz ), Department of Computer Science, University of Exeter, Exeter, 1997. (This paper describes the role logic plays in formal methods, including coverage of "computer program" verification through the use of propositions. A pathway from verification to automatic synthesis of programs from specifications is created.)

• TEMPORAL/COMPUTATIONAL LOGIC
  
  
  • Baral C., Barry M., Goal Specification using Temporal Logic in the Presense of Non-Deterministic Actions, ( ps.gz ), 2003.
  • Bellini P., Mattolini R., Nesi P., Temporal Logics for Real-Time System Specification ( pdf.gz ), ACM Computing Surveys, Vol. 32, No. 1, March 2000. (This paper contains an extensive discussion on a "whole family" of temporal logics suitable for the specification, validation and verification of real-time systems).
  • Sebastianli R., Introduction to Formal Methods for HW and SW Development 03: Temporal Logics ( pdf.gz ), A.A. 2003-2004, CDLS in Informatica (This tutorial is a very good introduction to linear and branching temporal logic.)

• MODELING TIMED SYSTEMS
  
  
  • Sidorova N., An Introduction to Process Modeling ( pdf.gz ). Lecture Notes in Process Modeling, Department of Mathematics and Computer Science, Technical University of Eindhoven, The Netherlands, 2004. (Explains how process modeling can be used to validate properties of systems early in the development phase).
  • Sidorova N., Specifying Requirements: Lecture 2 ( pdf.gz ). Lecture Notes in Process Modeling, Department of Mathematics and Computer Science, Technical University of Eindhoven, The Netherlands, 2004. (These notes provide a very nice introduction to the specification of requirements using temporal logics.)
  • Sidorova N., Modeling Timed Systems ( pdf.gz ). Lecture Notes in Process Modeling, Department of Mathematics and Computer Science, Technical University of Eindhoven, The Netherlands, 2004. (Covers the modeling of timed systems, e.g., discrete and dense time; introduction to timed automaton; guards vs invariants.)

• TIMED AUTOMATA
  
  
  • Slind K., Class Notes on Theory of Computation ( pdf.gz ), Department of Computer Science, University of Utah, October 2004. (An easy-to-read introduction to automata and the role of automata in models of computation).
  • Hooman J., An Introduction to Timed Systems ( pdf.gz ), ( ps.gz ), University of Nijmegen, Nov. 2001. (This short presentation is a nice overview of modeling for timed systems and associated design/analysis problems).
  • Tesei L., Specification and Verification using Timed Automata ( pdf.gz ), Ph.D. Thesis, Dipartmento di Informatika, Italy, 2004. (Chapter 2 of this Ph.D dissertation contains a nicely written overview of timed automata and, in particular, describes the timing model used by UPPAAL.)
  • Alur R. and Dill D.L., A Theory of Timed Automata ( ps.gz ), Department of Computer Science, Stanford University, CA, 1991. (This paper established the theoretical framework for timed automata).
  • Francois Laroussinie, Kim G. Larsen, and Carsten Weise, From Timed Automata to Logic and Back ( pdf.gz ), BRICS Report Series RS-95-2, Department of Computer Science University of Aarhus, Denmark, January 1995.

• SPATIAL DATA TYPES AND SPATIAL LOGIC
  
  
  • Randell D.A., Cui Z., Cohn A.G., A Spatial Logic based on Regions and Connectivity ( pdf.gz ), ( ps.gz ), Division of Artificial Intelligence, School of Computer Studies, Leeds University.
  • Damski J.C., Gero J.S., A Spatial Logic based on Regions and Connectivity ( pdf.gz ), Computer-Aided Design, Vol. 28, No. 3, pp. 169-181, 1996.

• APPLICATIONS INVOLVING SPATIAL LOGIC
  
  
  • Schneider M., Spatial Data Types: Conceptual Foundation for the Design and Implementation of Spatial Database Systems and GIS (pdf.gz) , FernUniversitat Hagen Praktische Informatik IV, D-58084 Hagen, Germany. E-mail: markus.schneider@fernuni-hagen.de. (Spatial data types provide a fundamental abstraction for modeling the geometric structure of objects in space, their relationships.gz, properties and operations. This tutorial takes the reader on a systematic development of spatial data types and spatial logic needed to build GIS applications.)
  • Ugur Murat Erdem, Stan Sclaroff, Automated Camera Layout to Satisfy Task-Specific and Floorplan-Specific Coverage Requirements (pdf.gz) , Computer Science Department, Boston University.

• REAL-TIME SYSTEMS
  
  
  • Moller M.O., Structure and Hierarchy in Real-Time Systems: Modeling and Analysis ( pdf.gz ), Ph.D. Thesis Defense, BRICS Ph.D. School, Denmark, 2002.
  • Natalia Sidorova, Modeling Timed Systems ( pdf.gz ), Lecture Notes on Process Modeling, Dept. of Mathematics and Computing Scence, Technische Universiteit Eindhoven, The Netherlands, 2003. (Topics include discrete and dense timing models; elements of timed automaton (e.g., guards and invariants), synchronous and asynchronous applications, modeling with SPIN).

• MODEL CHECKING
  
  
  • Alur R., Model Checking of Hierarchical State Machines ( pdf.gz ), Proceedings of the 6th ACM SIGSOFT International Symposium on Foundations of Software Engineering, Lake Buena Vista, Florida, United States pages 175-188, 1998.
  • Jha S., Model Checking Basics ( ps.gz ), Computer Science Department, University of Wisconson, Madison.
  • Mishra B., Notes on Model Checking ( ps.gz ), Courant Institute of Mathematical Sciences, NYU, April 28, 2003.
  • Knapp A. et al., Model Checking Timed UML Statecharts and Collaborations ( pdf.gz ), 2002. (This paper contains a nice description of the railroad crossing problem).

• APPLICATIONS OF MODEL CHECKING
  
  
  • Jain R., Model Checking of State/Event Systems for Control and Data Path Verification ( ps.gz ), BS Honours Thesis, IIT Kharagpur, India, May 2000. (This thesis contains a nice discussion of model checking for operation of a traffic light controller).
  • Laroussinie F. et al., CMC: A Tool for Compositional Model Checking of Real-Time Systems , ( ps.gz ), In Proc IFIP Joint International Conference of Formal Description Techniques and Protocol Specification, Testing and Verification, Kluwer Publications, pp. 439-456, 1988. (This paper describes a specification for model checking real-time systems described with timed autonoma. Systems are assembled through parallel composition of component-level behaviors. There's nice example of a railroad crossing).
  • Gurevich Y. Huggins J.K., The Railroad Crossing Problem: An Experiment with Instantaneous Actions and Immediate Reactions ( pdf.gz ), Computer Science Logics, May 2002.
  • Heitmeyer C. and Lynch N., The Generalized Railroad Crossing: A Case Study in Formal Verification of Real-Time Systems ( pdf.gz ). IEEE Real-Time Systems Symposium, 1994.
  • Knapp A. et al., Model Checking Timed UML Statecharts and Collaborations ( pdf.gz ), 2002. (This paper contains a nice description of the railroad crossing problem).

• VERIFICATION OF REAL-TIME SYSTEMS WITH UPPAAL
  
  
  • David A. and Amnell T., UPPAAL2k: Small Tutorial ( pdf.gz), October, 2002. (This document is a newcomers guide to Uppaal. The reader is walked step by step through the mutual exclusion problem. There's a nice explanation of how time concepts are modeled.)
    
  • Behrmann G., Alexandre David A., and Larsen K.G., A Tutorial on UPPAAL ( pdf.gz ), Department of Computer Science, Aalborg University, Denmark {behrmann,adavid,kgl}@cs.auc.dk. (A good introduction to modeling networks of timed automata in UPPAAL. Topics include: semantics of timed automata, semantics of networks of timed automata, the query language, understanding time, overview of the UPPAAL toolkit. Two examples are presented: (1) the generalized railroad crossing problem, and (2) Fischer's protocol, a well-known mutual exclusion protocol designed for n processes.)
    
  • Bengtsson J., Larson F., UPPAAL: A Tool for Verification of Real-Time Systems ( pdf.gz ), Department of Computer Systems, Upps.gzala University, Sweden, January, 1996.
  • Behrmann G., Larsen K.G., Verification of Non-Functional Properties ( pdf.gz ), Aalborg University, Denmark.
  • Larsen K.G., Petterson P. and Yi W., The model-checker UPPAAL ( pdf.gz ), The University of Birmingham.
  • Larsen K.G., Petterson P. and Yi W., UPPAAL In A Nutshell ( pdf.gz ), Department of Computer Science and Mathematics Aalborg University Denmark, Department of Computer Systems, Upps.gzala University, Sweden.
  • Kothavale M., Verifying a Burglar Alarm System with UPPAAL ( pdf.gz ), (This short presentation describes the model setup and verification procedure for a burglar alarm system using UPPAAL.)

Developed in August 2004 by Mark Austin
Copyright © 2004-2005, Institute for Systems Research, University of Maryland