- Authors:
- Tim Sheard,
- David Stemple
MAINTAINING THE INTEGRITY OF DATABASES IS ONE OF THE PROMISES OF DATABASE MANAGEMENT SYSTEMS. THIS INCLUDES ASSURING THAT INTEGRITY CONSTRAINTS ARE INVARIANTS OF DATABASE TRANSACTIONS. THIS IS VERY DIFFICULT TO ACCOMPLISH EFFICIENTLY IN THE PRESENCE OF COMPLEX CONSTRAINTS AND LARGE AMOUNTS OF DATA. ONE WAY TO MINIMIZE THE AMOUNT OF PROCESSING REQUIRED TO MAINTAIN DATABASE INTEGRITY OVER TRANSACTION PROCESSING IS TO PROVE AT COMPILE-TIME THAT TRANSACTIONS CANNOT, IF RUN ATOMICALLY, DISOBEY INTEGRITY CONSTRAINTS. WE REPORT ON A SYSTEM WHICH PERFORMS SUCH VERIFICATION FOR A ROBUST SET OF CONSTRAINT AND TRANSACTION CLASSES. THE SYSTEM ACCEPTS DATABASE SCHEMAS WRITTEN IN A MORE OR LESS TRADITIONAL STYLE AND ACCEPTS PROGRAMS IN A HIGH LEVEL PROGRAMMING LANGUAGE. AUTOMATIC VERIFICATION FAST ENOUGH TO BE EFFECTIVE ON CURRENT WORKSTATION HARDWARE IS PERFORMED.
Cited By
- Qian X and Waldinger R (1988). A transaction logic for database specification, ACM SIGMOD Record, 17:3, (243-250), Online publication date: 1-Jun-1988.
- Mazumdar S, Stemple D and Sheard T (1988). Resolving the tension between integrity and security using a theorem prover, ACM SIGMOD Record, 17:3, (233-242), Online publication date: 1-Jun-1988.
- Qian X and Waldinger R A transaction logic for database specification Proceedings of the 1988 ACM SIGMOD international conference on Management of data, (243-250)
- Mazumdar S, Stemple D and Sheard T Resolving the tension between integrity and security using a theorem prover Proceedings of the 1988 ACM SIGMOD international conference on Management of data, (233-242)
- Croft W and Stemple D (2019). Supporting office document architectures with constrained types, ACM SIGMOD Record, 16:3, (504-509), Online publication date: 1-Dec-1987.
- Stemple D, Mazumdar S and Sheard T (1987). On the modes and meaning of feedback to transaction designers, ACM SIGMOD Record, 16:3, (374-386), Online publication date: 1-Dec-1987.
- Croft W and Stemple D Supporting office document architectures with constrained types Proceedings of the 1987 ACM SIGMOD international conference on Management of data, (504-509)
- Stemple D, Mazumdar S and Sheard T On the modes and meaning of feedback to transaction designers Proceedings of the 1987 ACM SIGMOD international conference on Management of data, (374-386)
Recommendations
Automatic verification of database transaction safety
Maintaining the integrity of databases is one of the promises of database management systems. This includes assuring that integrity constraints are invariants of database transactions. This is very difficult to accomplish efficiently in the presence of ...
Testing database transaction concurrency
ASE'03: Proceedings of the 18th IEEE International Conference on Automated Software EngineeringDatabase application programs are often designed to be executed concurrently by many users. By grouping related database queries into transactions, DBMS systems can guarantee that each transaction satisfies the well-known ACID properties: Atomicity, ...