From 2c88912893ebbcc3b9fa14d4fcc100c42252d0df Mon Sep 17 00:00:00 2001
From: Andrew Butterfield <andrew.butterfield@scss.tcd.ie>
Date: Thu, 9 Nov 2023 11:26:56 +0000
Subject: eng: Add formal verification chapter

---
 common/refs.bib | 75 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 75 insertions(+)

(limited to 'common/refs.bib')

diff --git a/common/refs.bib b/common/refs.bib
index 066d746..e22dd6d 100644
--- a/common/refs.bib
+++ b/common/refs.bib
@@ -9,6 +9,23 @@
   year        = {1973},
   pages       = {46-61},
 }
+@article{Djikstra:1975:GCL,
+author = {Dijkstra, Edsger W.},
+title = {Guarded Commands, Nondeterminacy and Formal Derivation of Programs},
+year = {1975},
+issue_date = {Aug. 1975},
+publisher = {Association for Computing Machinery},
+address = {New York, NY, USA},
+volume = {18},
+number = {8},
+issn = {0001-0782},
+url = {https://doi.org/10.1145/360933.360975},
+doi = {10.1145/360933.360975},
+journal = {Commun. ACM},
+month = {aug},
+pages = {453–457},
+numpages = {5},
+}
 @inproceedings{Varghese:1987:TimerWheel,
   author      = {Varghese, G. and Lauck, T.},
   title       = {{Hashed and Hierarchical Timing Wheels: Data Structures for the Efficient Implementation of a Timer Facility}},
@@ -159,6 +176,31 @@
   year        = {2007},
   url         = {http://www.akkadia.org/drepper/cpumemory.pdf},
 }
+@article{Hierons:2009:FMT,
+  author    = {Robert M. Hierons and
+               Kirill Bogdanov and
+               Jonathan P. Bowen and
+               Rance Cleaveland and
+               John Derrick and
+               Jeremy Dick and
+               Marian Gheorghe and
+               Mark Harman and
+               Kalpesh Kapoor and
+               Paul J. Krause and
+               Gerald L{\"{u}}ttgen and
+               Anthony J. H. Simons and
+               Sergiy A. Vilkomir and
+               Martin R. Woodward and
+               Hussein Zedan},
+  title     = {Using formal specifications to support testing},
+  journal   = {{ACM} Comput. Surv.},
+  volume    = {41},
+  number    = {2},
+  pages     = {9:1--9:76},
+  year      = {2009},
+  url       = {https://doi.org/10.1145/1459352.1459354},
+  doi       = {10.1145/1459352.1459354},
+}
 @inproceedings{Mavin:2009:EARS,
   author      = {Mavin, Alistair and Wilkinson, Philip and Harwood, Adrian and Novak, Mark},
   title       = {{Easy approach to requirements syntax (EARS)}},
@@ -369,6 +411,39 @@
   doi         = {10.1109/RE.2016.38},
   url         = {https://www.researchgate.net/profile/Alistair_Mavin/publication/308970788_Listens_Learned_8_Lessons_Learned_Applying_EARS/links/5ab0d42caca2721710fe5017/Listens-Learned-8-Lessons-Learned-Applying-EARS.pdf},
 }
+@manual{Butterfield:2021:FV1-200,
+  author       = {Andrew Butterfield and Mike Hinchey},
+  organization = {Lero -- the Irish Software Research Centre},
+  title        = {FV1-200: Formal Verification Plan},
+  year         = {2021}
+}
+@mastersthesis{Jennings:2021:FV,
+  author =       {Robert Jennings},
+  title =        {{Formal Verification of a Real-Time Multithreaded Operating System}},
+  school =       {School of Computer Science and Statistics},
+  year =         {2021},
+  type =         {Master of Science in {Computer Science (MCS)}},
+  address =      {Trinity College, Dublin 2, Ireland},
+  month =        {August},
+}
+@mastersthesis{Jaskuc:2022:TESTGEN,
+  author =       {Jerzy Ja{\'{s}}ku{\'{c}}},
+  title =        {{SPIN/Promela-Based Test Generation Framework for RTEMS Barrier Manager}},
+  school =       {School of Computer Science and Statistics},
+  year =         {2022},
+  type =         {Master of Science in {Computer Science (MCS)}},
+  address =      {Trinity College, Dublin 2, Ireland},
+  month =        {April},
+}
+@mastersthesis{Lynch:2022:TESTGEN,
+  author =       {Eoin Lynch},
+  title =        {{Using Promela/SPIN to do Test Generation for RTEMS-SMP}},
+  school =       {School of Engineering},
+  year =         {2022},
+  type =         {Master of {Engineering (Computer Engineering)}},
+  address =      {Trinity College, Dublin 2, Ireland},
+  month =        {April},
+}
 @misc{RTEMS:CPU,
   title     = {{RTEMS CPU Architecture Supplement}},
   url       = {https://docs.rtems.org/branches/master/cpu-supplement.pdf},
-- 
cgit v1.2.3