Click on a search word OR use the drop-down choices to search for a paper.
2021
Diskin, Zinovy; Stunkel, Patrick
Sketches, Queries, and Views: From Term-Graphs to Diagrammatic Term-Sketches Technical Report
2021.
Links | BibTeX | Tags: diagrammatic operations, formal verification, Kleisli, model management, software engineering, term-graphs
@techreport{Diskin2021,
title = {Sketches, Queries, and Views: From Term-Graphs to Diagrammatic Term-Sketches},
author = {Zinovy Diskin and Patrick Stunkel},
url = {https://www.mcscert.ca/wp-content/uploads/2021/06/McSCert-Technical-Report-34.pdf},
year = {2021},
date = {2021-05-11},
urldate = {2021-05-11},
keywords = {diagrammatic operations, formal verification, Kleisli, model management, software engineering, term-graphs},
pubstate = {published},
tppubtype = {techreport}
}
2015
Pang, Linna; Wang, Chen-Wei; Lawford, Mark; Wassyng, Alan
Formal verification of function blocks applied to IEC 61131-3 Journal Article
In: Science of Computer Programming, vol. 113, no. Part 2, pp. 149–190, 2015.
BibTeX | Tags: critical systems, formal verification, function blocks, IEC 61131-3, tabular expression
@article{pang2015formalb,
title = {Formal verification of function blocks applied to IEC 61131-3},
author = {Pang, Linna and Wang, Chen-Wei and Lawford, Mark and Wassyng, Alan},
year = {2015},
date = {2015-01-01},
journal = {Science of Computer Programming},
volume = {113},
number = {Part 2},
pages = {149--190},
publisher = {Elsevier},
keywords = {critical systems, formal verification, function blocks, IEC 61131-3, tabular expression},
pubstate = {published},
tppubtype = {article}
}
Pang, Linna; Wang, Chen-Wei; Lawford, Mark; Wassyng, Alan; Newell, Josh; Chow, Vera; Tremaine, David
Formal Verification of Real-Time Function Blocks Using PVS Proceedings Article
In: 4th International Workshop on Engineering Safety and Security Systems 2015 (ESSS’15), pp. 65–79, Electronic Proceedings in Theoretical Computer Science 2015.
BibTeX | Tags: formal verification, function blocks, IEC 61131-3, safety-critical systems, software certification
@inproceedings{pang2015formal,
title = {Formal Verification of Real-Time Function Blocks Using PVS},
author = {Pang, Linna and Wang, Chen-Wei and Lawford, Mark and Wassyng, Alan and Newell, Josh and Chow, Vera and Tremaine, David},
year = {2015},
date = {2015-01-01},
booktitle = {4th International Workshop on Engineering Safety and Security Systems 2015 (ESSS’15)},
volume = {184},
pages = {65--79},
organization = {Electronic Proceedings in Theoretical Computer Science},
keywords = {formal verification, function blocks, IEC 61131-3, safety-critical systems, software certification},
pubstate = {published},
tppubtype = {inproceedings}
}
2003
Zhang, Hong
SQRL Report No. 17 “Formal Verification of Timed Transition Models” Technical Report
2003.
Abstract | Links | BibTeX | Tags: formal verification, timed transition model
@techreport{Zhang2003,
title = {SQRL Report No. 17 “Formal Verification of Timed Transition Models”},
author = {Hong Zhang},
url = {http://www.cas.mcmaster.ca/sqrl/papers/sqrl17.pdf},
year = {2003},
date = {2003-11-15},
abstract = {Labeled Transition Systems (LTSs) are used to express specifications and implementations of software. State-Event Labeled Transition Systems (SELTS's) extend LTS's by adding a state output map and an event map. A Timed Transition Model (TTM) is a timed extension of SELTS. The extension involves lower and upper time bound constraints and transitions, that relate to the number of occurrences of the special transition tick. A TTM can be described as a SELTS with a timer attached to each different transition, so that we can specify the time requirements of the model. This thesis gives the definitions of invariants, strong equivalence and weak equivalence for SELTSs and TTMs in PVS. It also provides a unified modeling environment for SELTSs and TTMs in PVS which allows the user to specify them easily. Further, the thesis illustrates the use of the modeling environment in PVS to prove invariants, weak equivalence and strong equivalence of SELTS s and TTM s by providing one example in each category. Finally we use our modeling environment to fomalise and verify the correctness on an industrial real-time controller.
Our method has the advantage that is simplifies the procedure for translating SELTS and TTMs into PVS. A disadvantage is that it still needs a number of interactions between the user and PVS, although some of theses could be considered as routine work.},
keywords = {formal verification, timed transition model},
pubstate = {published},
tppubtype = {techreport}
}
Our method has the advantage that is simplifies the procedure for translating SELTS and TTMs into PVS. A disadvantage is that it still needs a number of interactions between the user and PVS, although some of theses could be considered as routine work.