Specification and Formal Verification of Atomic Concurrent Real-Time Transactions
2018 IEEE 23rd Pacific Rim International Symposium on Dependable Computing (PRDC)(2018)
摘要
Although atomicity, isolation and temporal correctness are crucial to the dependability of many real-time database-centric systems, the selected assurance mechanism for one property may breach another. Trading off these properties requires to specify and analyze their dependencies, together with the selected supporting mechanisms (abort recovery, concurrency control, and scheduling), which is still insufficiently supported. In this paper, we propose a UML profile, called UTRAN, for specifying atomic concurrent real-time transactions, with explicit support for all three properties and their supporting mechanisms. We also propose a pattern-based modeling framework, called UPPCART, to formalize the transactions and the mechanisms specified in UTRAN, as UPPAAL timed automata. Various mechanisms can be modeled flexibly using our reusable patterns, after which the desired properties can be verified by the UPPAAL model checker. Our techniques facilitate systematic analysis of atomicity, isolation and temporal correctness trade-offs with guarantee, thus contributing to a dependable real-time database system.
更多查看译文
关键词
Unified modeling language,Real-time systems,Automata,Analytical models,Concurrency control,Database systems,Data models
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络