Browsing Mathematics (Faculty of) by Subject "Model Checking"
Now showing items 1-6 of 6
-
Applications of Description Logic and Causality in Model Checking
(University of Waterloo, 2009-06-19)Model checking is an automated technique for the verification of finite-state systems that is widely used in practice. In model checking, a model M is verified against a specification $\varphi$, exhaustively checking ... -
Automated Analysis of Unified Modeling Language (UML) Specifications
(University of Waterloo, 2001)The Unified Modeling Language (UML) is a standard language adopted by the Object Management Group (OMG) for writing object-oriented (OO) descriptions of software systems. UML allows the analyst to add class-level and ... -
Mapping Template Semantics to SMV
(University of Waterloo, 2004)Template semantics is a template-based approach to describing the semantics of model-based notations, where a pre-defined template captures the notations' common semantics, and parameters specify the notations' distinct ... -
Symmetry Reduction and Compositional Verification on Timed Automata
(University of Waterloo, 2017-08-24)This thesis is about techniques for the analysis of concurrent and real-time systems. As the first contribution, we describe a technique that incorporates automatic symmetry detection and symmetry reduction in the ... -
Using Software Model Checking for Software Certification
(University of Waterloo, 2010-09-13)Software certification is defined as the process of independently confirming that a system or component complies with its specified requirements and is acceptable for use. It consists of the following steps: (1) the ... -
Verifying Mutable Systems
(University of Waterloo, 2017-10-23)Model checking has had much success in the verification of single-process and multi-process programs. However, model checkers assume an immutable topology which limits the verification in several areas. Consider the security ...