Click on a search word OR use the drop-down choices to search for a paper.
2021
Singh, Neeraj Kumar; Lawford, Mark; Maibaum, Tom; Wassyng, Alan
A formal approach to rigorous development of critical systems Journal Article
In: Journal of Software: Evolution and Process, 2021.
Abstract | Links | BibTeX | Tags: certification, code generation, formal methods, proof‐based development, refinement, simulation, tabular expression, verification and validation
@article{Singh2021,
title = {A formal approach to rigorous development of critical systems},
author = {Neeraj Kumar Singh and Mark Lawford and Tom Maibaum and Alan Wassyng},
doi = { https://doi.org/10.1002/smr.2334},
year = {2021},
date = {2021-01-26},
urldate = {2021-01-26},
journal = {Journal of Software: Evolution and Process},
abstract = {Safety critical systems, such as medical, automotive, and avionics systems, play an important role in our daily lives. Increasing demand for new technologies in these safety critical systems requires rapid adoption of commercial hardware and software. However, the adoption of new hardware and software increases life‐threatening vulnerabilities. To aid in the reduction of these vulnerabilities and system failures, this paper proposes a framework based on formal methods for developing safety‐critical systems from requirements analysis to code generation. This framework includes a development process for documenting system requirements using tabular expressions, automatic formal model generation from the documented requirements, verification and validation of the generated formal models using proof techniques and animations, interactive simulation for validating the required behavior of the developed models by enabling domain experts to observe the system states according to, and finally, code generation from the formal model into a desired language. A prototype toolchain is developed to automate this framework. An assessment of the proposed framework is undertaken through a case study: insulin infusion pump (IIP).},
keywords = {certification, code generation, formal methods, proof‐based development, refinement, simulation, tabular expression, verification and validation},
pubstate = {published},
tppubtype = {article}
}
2017
Mohammad Gholizadeh, Hamid
A Query Structured Model Transformation Approach PhD Thesis
McMaster University, 2017.
Abstract | Links | BibTeX | Tags: Diagrammatic Queries, formal methods, Model Synchronization Taxonomy, model transformation
@phdthesis{Gholizadeh2017,
title = {A Query Structured Model Transformation Approach},
author = {Mohammad Gholizadeh, Hamid},
url = {https://www.mcscert.ca/mohammadgholizadeh_hamid_201706_phd/},
year = {2017},
date = {2017-10-03},
school = {McMaster University},
abstract = {Model Driven Engineering (MDE) has gained a considerable attention in the software engineering domain in the past decade. MDE proposes shifting the focus of the engineers from concrete artifacts (e.g., code) to more abstract structures (i.e., models). Such a change allows using the human intelligence more efficiently in engineering software products. Model Transformation (MT) is one of the key operations in MDE and plays a critical role in its successful application. The current MT approaches, however, usually miss either one or both of the two essential features: 1) declarativity in the sense that the MT definitions should be expressed at a sufficiently high level of abstraction, and 2) formality in the sense that the approaches should be based on precise underlying semantics. These two features are both critical in effectively managing the complexity of a network of interrelated models in an MDE process. This thesis tackles these shortcomings by promoting a declarative MT approach that is built on mathematical foundations. The approach is called Query Structured Transformation (QueST) as it proposes a structured orchestration of diagrammatic queries in the MT definitions. The aim of the thesis is to make the QueST approach –that is based on formal foundations– accessible to the MDE community. This thesis first motivates the necessity of having declarative formal approaches by studying the variety of model synchronization scenarios in the networks of interrelated models. Then, it defines a diagrammatic query framework (DQF) that formulates the syntax and the semantics of the QueST collection-level diagrammatic operations. By a detailed comparison of the QueST approach and three rule-based MT approaches (ETL, ATL, and QVT-R), the thesis shows the way QueST contributes to the development of the following aspects of MT definitions: declarativity, modularity, incrementality, and logical analysis of MT definitions.},
keywords = {Diagrammatic Queries, formal methods, Model Synchronization Taxonomy, model transformation},
pubstate = {published},
tppubtype = {phdthesis}
}
2015
Singh, Neeraj Kumar; Lawford, Mark; Maibaum, Thomas SE; Wassyng, Alan
Formalizing the Cardiac Pacemaker Resynchronization Therapy Proceedings Article
In: International Conference on Digital Human Modeling and Applications in Health, Safety, Ergonomics and Risk Management, pp. 374–386, Springer International Publishing 2015.
BibTeX | Tags: event-B, formal methods, pacemaker, pacemaker resynchronization therapy, refinement, validation, verification
@inproceedings{singh2015formalizing,
title = {Formalizing the Cardiac Pacemaker Resynchronization Therapy},
author = {Singh, Neeraj Kumar and Lawford, Mark and Maibaum, Thomas SE and Wassyng, Alan},
year = {2015},
date = {2015-01-01},
booktitle = {International Conference on Digital Human Modeling and Applications in Health, Safety, Ergonomics and Risk Management},
pages = {374--386},
organization = {Springer International Publishing},
keywords = {event-B, formal methods, pacemaker, pacemaker resynchronization therapy, refinement, validation, verification},
pubstate = {published},
tppubtype = {inproceedings}
}
Singh, Neeraj Kumar; Wang, Hao; Lawford, Mark; Maibaum, Thomas SE; Wassyng, Alan
Stepwise Formal Modelling and Reasoning of Insulin Infusion Pump Requirements Proceedings Article
In: International Conference on Digital Human Modeling and Applications in Health, Safety, Ergonomics and Risk Management, pp. 387–398, Springer International Publishing 2015.
BibTeX | Tags: event-B, formal methods, insulin infusion pump, refinement, validation, verification
@inproceedings{singh2015stepwise,
title = {Stepwise Formal Modelling and Reasoning of Insulin Infusion Pump Requirements},
author = {Singh, Neeraj Kumar and Wang, Hao and Lawford, Mark and Maibaum, Thomas SE and Wassyng, Alan},
year = {2015},
date = {2015-01-01},
booktitle = {International Conference on Digital Human Modeling and Applications in Health, Safety, Ergonomics and Risk Management},
pages = {387--398},
organization = {Springer International Publishing},
keywords = {event-B, formal methods, insulin infusion pump, refinement, validation, verification},
pubstate = {published},
tppubtype = {inproceedings}
}
Gruner, Stefan; Kumar, Apurva; Maibaum, Tom
Towards a Body of Knowledge in Formal Methods for the Railway Domain: Identification of Settled Knowledge Proceedings Article
In: International Workshop on Formal Techniques for Safety-Critical Systems, pp. 87–102, Springer 2015.
BibTeX | Tags: body of knowledge, formal concept analysis, formal methods, railway domain, semantic lattices, settled knowledge
@inproceedings{gruner2015towards,
title = {Towards a Body of Knowledge in Formal Methods for the Railway Domain: Identification of Settled Knowledge},
author = {Gruner, Stefan and Kumar, Apurva and Maibaum, Tom},
year = {2015},
date = {2015-01-01},
booktitle = {International Workshop on Formal Techniques for Safety-Critical Systems},
pages = {87--102},
organization = {Springer},
keywords = {body of knowledge, formal concept analysis, formal methods, railway domain, semantic lattices, settled knowledge},
pubstate = {published},
tppubtype = {inproceedings}
}
2007
Leduc, Ryan J; Dai, Pengcheng; Song, Raoguang
SQRL Report No. 46 “Synthesis Method for Hierarchical Interface-Based Supervisory Control.” Technical Report
2007.
Abstract | Links | BibTeX | Tags: automata, discrete-event systems, formal methods, hierarchical systems, interfaces, supervisory control, synthesis
@techreport{LeducDaiSong2007,
title = {SQRL Report No. 46 “Synthesis Method for Hierarchical Interface-Based Supervisory Control.”},
author = {Ryan J Leduc and Pengcheng Dai and Raoguang Song},
url = {http://www.cas.mcmaster.ca/sqrl/papers/SQRLreport46.pdf},
year = {2007},
date = {2007-08-15},
abstract = {Hierarchical Interface-Based Supervisory Control (HISC) decomposes a discrete-event system (DES) into a high-level subsystem which communicates with n >= 1 low-level subsystems, through separate interfaces. It provides a set of local conditions that can be used to verify global conditions such as nonblocking and controllability such that the complete system model never needs to be constructed.
Currently, a designer must create the supervisors himself and then verify that they satisfy the HISC conditions. In this paper, we develop a synthesis method that can take advantage of the HISC structure. We replace the supervisor for each level by a corresponding specification DES. We then construct for each level a maximally permissive supervisor that satisfies the corresponding HISC conditions.
We define a set of language based fixpoint operators and show that they compute the required level-wise supremal languages. We then discuss the complexity of our algorithms and show that they potentially offer significant savings over the monolithic approach. We also briefly discuss a symbolic HISC verification and synthesis method using Binary Decision Diagrams, that we have also developed.
A large manufacturing system example (worst case state space on the order of 10^30) extended from the AIP example is briefly discussed. The example showed that we can now handle a given level with a statespace as large as 10^15 states, using less than 160MB of memory. This represents a significant improvement in the size of systems that can be handled by the HISC approach. A software tool for synthesis and verification of HISC systems using our approach was also developed.},
keywords = {automata, discrete-event systems, formal methods, hierarchical systems, interfaces, supervisory control, synthesis},
pubstate = {published},
tppubtype = {techreport}
}
Currently, a designer must create the supervisors himself and then verify that they satisfy the HISC conditions. In this paper, we develop a synthesis method that can take advantage of the HISC structure. We replace the supervisor for each level by a corresponding specification DES. We then construct for each level a maximally permissive supervisor that satisfies the corresponding HISC conditions.
We define a set of language based fixpoint operators and show that they compute the required level-wise supremal languages. We then discuss the complexity of our algorithms and show that they potentially offer significant savings over the monolithic approach. We also briefly discuss a symbolic HISC verification and synthesis method using Binary Decision Diagrams, that we have also developed.
A large manufacturing system example (worst case state space on the order of 10^30) extended from the AIP example is briefly discussed. The example showed that we can now handle a given level with a statespace as large as 10^15 states, using less than 160MB of memory. This represents a significant improvement in the size of systems that can be handled by the HISC approach. A software tool for synthesis and verification of HISC systems using our approach was also developed.
2003
He, Yu-Tong
SQRL Report No. 10 “Verification of the WAP Transaction Layer Using the Model Checker SPIN” Technical Report
2003.
Abstract | Links | BibTeX | Tags: formal methods, transaction layer protocol
@techreport{He2003,
title = {SQRL Report No. 10 “Verification of the WAP Transaction Layer Using the Model Checker SPIN”},
author = {Yu-Tong He},
url = {http://www.cas.mcmaster.ca/sqrl/papers/YTR.pdf},
year = {2003},
date = {2003-08-15},
abstract = {This report presents a formal methodology of formalizing and verifying the Transaction Layer Protocol (WTP) design in the Wireless Application Protocol (WAP) architecture. Corresponding to the Class 2 Transaction Service (TR-Service) definition and the Protocol (TR-Protocol) design, two models at different abstraction levels are built with a finite state automation (FSA) formalism. By using the model checker SPIN, we uncover defects in a latest approved version of the TR-Protocol design, which can lead to deadlock, channel buffer overflow and unfaithful refinement of the TR-Service definition. As an extended result, a set of safety, liveness and temporal properties is verified for the WTP to be operating in a more general environment which allows for loss and re-ordering messages.},
keywords = {formal methods, transaction layer protocol},
pubstate = {published},
tppubtype = {techreport}
}
1997
Bicarregui, JC; Lano, KC; Maibaum, TSE
Towards a Compositional Interpretation of Object Diagrams Journal Article
In: Algorithimic Languages and Calculi, pp. 187, 1997.
BibTeX | Tags: action logic, encapsulation, formal methods, object calculus, temporal logic
@article{bicarreguitextordmasculine2016towards,
title = {Towards a Compositional Interpretation of Object Diagrams},
author = {Bicarregui, JC and Lano, KC and Maibaum, TSE},
year = {1997},
date = {1997-12-31},
journal = {Algorithimic Languages and Calculi},
pages = {187},
publisher = {Springer},
keywords = {action logic, encapsulation, formal methods, object calculus, temporal logic},
pubstate = {published},
tppubtype = {article}
}