Search
for Topics
All Reviews
Browse All Reviews
>
Software (D)
>
Software Engineering (D.2)
>
Software/Program Verification (D.2.4)
> Model Checking (D.2.4...)
Options:
All Media Types
Journals
Proceedings
Div Books
Whole Books
Other
Date Reviewed
Title
Author
Publisher
Published Date
Descending
Ascending
1-10 of 43 Reviews about "
Model Checking (D.2.4...)
":
Date Reviewed
Handbook of model checking
Clarke E., Henzinger T., Veith H., Bloem R., Springer International Publishing, New York, NY, 2018. 1210 pp. Type: Book (978-3-319105-74-1)
Due to the proliferation and pervasiveness of hardware and software entities in everyday life, ascertaining their trustworthiness is of paramount importance. Model checking is a logic-based approach that determines whether the abstract...
May 20 2019
Model-based testing of probabilistic systems
Gerhold M., Stoelinga M. Formal Aspects of Computing 30(1): 77-106, 2018. Type: Article
Gerhold and Stoelinga’s paper proposes an interesting framework to test probabilistic systems based on the concepts of soundness and completeness. The crux of their argument is “the conformance relation for probabil...
Apr 18 2018
Incremental bounded model checking for embedded software
Schrammel P., Kroening D., Brain M., Martins R., Teige T., Bienmüller T. Formal Aspects of Computing 29(5): 911-931, 2017. Type: Article
Bounded model checking is employed in tools for the formal verification of C programs such as the C bounded model checker (CBMC). The key idea of this technique is to unwind unbounded program loops to a fixed depth and to translate the...
Dec 4 2017
Model checking learning agent systems using Promela with embedded C code and abstraction
Kirwan R., Miller A., Porr B. Formal Aspects of Computing 28(6): 1027-1056, 2016. Type: Article
Model checking is a formal method that decides whether a system satisfies a property formulated in temporal logic. While model checking is typically applied to hardware/software systems, it may be used to analyze any system that reache...
Mar 29 2017
Rigorous modeling and analysis of interoperable medical devices
Mashkoor A., Sametinger J. MSM 2016 (Proceedings of the Modeling and Simulation in Medicine Symposium, Pasadena, CA, Apr 3-6, 2016) 1-8, 2016. Type: Proceedings, Reviews: (2 of 2)
“First, do no harm” meets the Internet of Things (IoT)? This paper proposes that we need to be sure that medical systems are functional, safe, and secure--of course. Further, the authors try to show how the...
Aug 19 2016
Rigorous modeling and analysis of interoperable medical devices
Mashkoor A., Sametinger J. MSM 2016 (Proceedings of the Modeling and Simulation in Medicine Symposium, Pasadena, CA, Apr 3-6, 2016) 1-8, 2016. Type: Proceedings, Reviews: (1 of 2)
With the advent of the electronic health record (EHR), the quality of patient care increased. Many hospitals are encouraging patients to voluntarily provide their own health status (patient health record, PHR) to be used by doctors whe...
Aug 18 2016
Optimising the ProB model checker for B using partial order reduction
Dobrikov I., Leuschel M. Formal Aspects of Computing 28(2): 295-323, 2016. Type: Article
Model checking is a way to see if a design meets requirements. It starts with a model that abstracts how events affect a system. Then, the designers formulate a required behavior, for example, that something will never happen. The chec...
Jun 20 2016
Towards personalized prostate cancer therapy using delta-reachability analysis
Liu B., Kong S., Gao S., Zuliani P., Clarke E. HSCC 2015 (Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control, Seattle, WA, Apr 14-16, 2015) 227-232, 2015. Type: Proceedings
In 2005, I was diagnosed with prostate cancer. This paper fits what I learned: one faces difficult choices because each cancer is different and there are many treatment options. This paper focuses on the hormone treatment that shuts do...
Jun 17 2015
Bounded model-checking of discrete duration calculus
Zu Q., Zhang M., Zhu J., Zhan N. HSCC 2013 (Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control, Philadelphia, PA, Apr 8-11, 2013) 213-222, 2013. Type: Proceedings
In the model-checking community, asserting the soundness of a finite-state model is achieved by verifying the model against appropriate mathematical specifications. The duration calculus is an interval temporal logic for defining speci...
Oct 10 2013
Alloy meets the Algebra of Programming: a case study
Oliveira J., Ferreira M. IEEE Transactions on Software Engineering 39(3): 305-326, 2013. Type: Article
Using a journaled file system operation refinement, the authors of this paper assert that future software development should be centered around readable documentation containing rigorous high-level mathematical specifications and calcu...
Sep 6 2013
Display
5
10
15
25
50
100
per page
Reproduction in whole or in part without permission is prohibited. Copyright 1999-2024 ThinkLoud
®
Terms of Use
|
Privacy Policy