Logic Summer School 2022
Some useful resources:
Hoare Logic and Rely/Guarantee Reasoning
- de Roever, W.-P. Concurrency. Introduction to Compositional and Non-compositional Methods,
Cambridge University Press, (2001). Chapter 9 introduces Hoare logic along with some good problems to work on.
Rely/guarantee is also covered. This book is very useful.
-
Hayes, I.J. and Jones, C.B. A Guide to Rely/Guarantee Thinking, Engineering Trustworthy Software Systems (SETSS 2017), Lecture Notes in Computer Science,
Vol.11174, pp.1-38, Springer, Cham., (2018).
Download from Springer.
- Jones, C. B. and Yatapanage, N. Investigating the limits of rely/guarantee relations based on a concurrent garbage collector example,
Formal Aspects of Computing. 31(3): 353-374. (2019).
Download from Springer.
-
Jones, C.B. and Yatapanage, N. Reasoning about Separation using Abstraction and Reification, 13th IEEE International
Conference on Software Engineering and Formal Methods (SEFM 2015), Lecture Notes in Computer Science,
Vol.9276, pp.3-19, Springer-Verlag, (2015).
Download from Springer.
Also take a look at the references on Cliff B. Jones' page.
Model checking for automating failure analysis and related topics
-
Baier, C. and Katoen, J.-P. Principles of model checking. MIT Press. (2008).
-
Huth, M. and Ryan, M. D. Logic in computer science - modelling and reasoning about systems. Cambridge University Press. (2000).
-
Grunske, L., Winter, K., Yatapanage,
N., Zafar, S. and Lindsay, P.A. Experience with Fault Injection
Experiments for FMEA, Journal of Software: Practice and Experience. 41(11):1233-1258. (2011).
Download from Wiley.
See the tech reports and model checking results.
-
Grunske, L., Winter, K.
and Yatapanage, N. Defining the Abstract Syntax of Visual Languages with
Advanced Graph Grammars - A Case Study Based on Behavior Trees,
Journal of Visual Languages and Computing. 19(3):343-379. (2008).
Download from ScienceDirect.
-
Grunske, L., Lindsay, P., Yatapanage, N. and Winter, K. An
Automated Failure Mode and Effect Analysis based on High-Level Design
Specification with Behavior Trees, Integrated Formal Methods: 5th
International Conference (IFM 2005), Proceedings. LNCS.
Springer-Verlag, Vol.3771, pp.129-149, 2005. Download from Springer
-
Lindsay, P., Winter, K.
and Yatapanage, N. Safety Assessment Using Behavior Trees and Model
Checking, 8th IEEE International Conference on Software Engineering and
Formal Methods (SEFM 2010), Proceedings. IEEE Computer Society,
pp.181-190, 2010. Download from IEEE
Slides
-
Wednesday lecture 1 (Hoare logic).
-
Wednesday lecture 2 (Intro to Concurrency).
-
Thursday lectures. The slides cover three interesting applications where rely/guarantee was used. We'll also go through a simple example on the board. You'll also need references (3) and (4) above.
-
Friday lectures. To see the moving demonstration of the industrial metal press, look at the Powerpoint version in Slideshow view: Powerpoint version. These lectures were on LTL, CTL*, using model checking to automate failure analysis, using graph grammar rules to create a translator between a specification language and a model checker, and next-preserving branching bisimulation. Note that the graph grammar part is not on the slides; look at reference (4) in the model checking section above. We also looked at a demonstration of a tool which translates Behavior Tree specifications to a model checking language.
|