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}
}
2020
Annable, Nicholas
A Model-Based Approach to Formal Assurance Cases Masters Thesis
McMaster University, 2020.
Abstract | Links | BibTeX | Tags: safety assurance, software engineering
@mastersthesis{Annable2020,
title = {A Model-Based Approach to Formal Assurance Cases},
author = {Annable, Nicholas},
url = {http://hdl.handle.net/11375/25343},
year = {2020},
date = {2020-03-20},
school = {McMaster University},
abstract = {The rapidly increasing complexity of safety-critical embedded systems has been the cause of difficulty in assuring the safety of safety-critical embedded systems and managing their documentation. More specifically, current approaches to safety assurance are struggling to keep up with the complex relationships be- tween the ever growing number of components and the sheer amount of code underlying safety-critical embedded systems such as road vehicles. We believe that an approach to safety assurance able to cope with this complexity must: i) have sound mathematical foundations on which safety assurance can be built; and ii) provide a formal framework with precisely defined semantics in which the assurance can be represented. In doing this, assurance can be made less ad-hoc, more precise and more repeatable. Sound mathematical foundations also facilitate the creation of tools that automate many aspects of assurance, which will be invaluable in coping with the complexity of modern-day and future embedded systems. The model-based framework that achieves this is + Workflow . This framework is rigorous, developed on proven notations from model-based methodologies, comprehensively integrates assurance within the development activities, and provides the basis for more formal assurance cases.},
keywords = {safety assurance, software engineering},
pubstate = {published},
tppubtype = {mastersthesis}
}
2015
Pantelic, Vera; Postma, Steven; Lawford, Mark; Korobkine, Alexandre; Mackenzie, Bennett; Ong, Jeff; Bender, Marc
A Toolset for Simulink: Improving Software Engineering Practices in Development with Simulink Proceedings Article
In: 3rd International Conference on Model-Driven Engineering and Software Development (MODELSWARD 2015), pp. 50–61, SCITEPRESS 2015.
BibTeX | Tags: data flow, Simulink, software engineering, tools, transformation
@inproceedings{pantelic2015toolset,
title = {A Toolset for Simulink: Improving Software Engineering Practices in Development with Simulink},
author = {Pantelic, Vera and Postma, Steven and Lawford, Mark and Korobkine, Alexandre and Mackenzie, Bennett and Ong, Jeff and Bender, Marc},
year = {2015},
date = {2015-01-01},
booktitle = {3rd International Conference on Model-Driven Engineering and Software Development (MODELSWARD 2015)},
pages = {50--61},
organization = {SCITEPRESS},
keywords = {data flow, Simulink, software engineering, tools, transformation},
pubstate = {published},
tppubtype = {inproceedings}
}
Bender, Marc; Laurin, Karen; Lawford, Mark; Pantelic, Vera; Korobkine, Alexandre; Ong, Jeff; Mackenzie, Bennett; Bialy, Monika; Postma, Steven
Signature required: Making Simulink data flow and interfaces explicit Journal Article
In: Science of Computer Programming, vol. 113, no. Part 1, pp. 29–50, 2015.
BibTeX | Tags: data flow, interfaces, model transformation, Simulink, software engineering
@article{bender2015signature,
title = {Signature required: Making Simulink data flow and interfaces explicit},
author = {Bender, Marc and Laurin, Karen and Lawford, Mark and Pantelic, Vera and Korobkine, Alexandre and Ong, Jeff and Mackenzie, Bennett and Bialy, Monika and Postma, Steven},
year = {2015},
date = {2015-01-01},
journal = {Science of Computer Programming},
volume = {113},
number = {Part 1},
pages = {29--50},
publisher = {Elsevier},
keywords = {data flow, interfaces, model transformation, Simulink, software engineering},
pubstate = {published},
tppubtype = {article}
}
2014
Xu, Hao
Model Based System Consistency Checking Using Event-B Masters Thesis
McMaster University, 2014.
Abstract | Links | BibTeX | Tags: event-B, formal specification, insulin infusion pump, safety constraints, safety critical systems, software engineering, timing constraints
@mastersthesis{Xu2014,
title = {Model Based System Consistency Checking Using Event-B},
author = {Xu, Hao},
url = {https://www.mcscert.ca/xu-hao-master-thesis-2011/},
year = {2014},
date = {2014-06-18},
school = {McMaster University},
abstract = {Formal methods such as Event-B are a widely used approach for developing critical systems. This thesis demonstrates that creating models and proving the consistency of the models at the requirements level during software (system) development is an effective way to reduce the occurrence of faults and errors in a practical application. An insulin infusion pump (IIP) is a complicated and time critical system. This thesis uses Event-B to specify models for an IIP, based on a draft requirements document developed by the US Food and Drug Administration (FDA). Consequently it demonstrates Event-B can be used effectively to detect the missing properties, the missing quantities, the faults and the errors at the requirements level of a system development. The IIP is an active and reactive time control system. To achieve the goal of handling timing issues in the IIP system, we made extensions of an existing time pattern specified using Event-B to enrich the semantics of the Event-B language. We created several sets to model the activation times of different events and the union of these time sets defines a global time activation set. The tick of global time is specified as a progress tick event. All the actions in an event are triggered only when the global time in the time tick event matches the time specified in the event. Time is deleted from the corresponding time set, but not the corresponding global time set while the event is triggered. A time point is deleted from the global time set only when there are no pending actions for that time point. Through discharging proof obligations using Event-B, we achieved our goal of improving the requirements document.},
keywords = {event-B, formal specification, insulin infusion pump, safety constraints, safety critical systems, software engineering, timing constraints},
pubstate = {published},
tppubtype = {mastersthesis}
}
2002
Parnas, DL; Soltys, Michael
SQRL Report No. 7 “Basic Science for Software Developers” Technical Report
2002.
Abstract | Links | BibTeX | Tags: software engineering
@techreport{Parnas2002b,
title = {SQRL Report No. 7 “Basic Science for Software Developers”},
author = {DL Parnas and Michael Soltys },
url = {http://www.cas.mcmaster.ca/sqrl/papers/sqrl7.pdf},
year = {2002},
date = {2002-10-15},
abstract = {This paper discusses the issue of what constitutes "basic science" for a Software Engineering programme. Accredited Enginering programmes all have a significant "basic science" component. For traditional Engineering disciplines, this covers the physical Sciences. While the physical sciences are also relevant for Engineers specialising in software intensive products, additional material is relevant. This paper proposes that certain areas of "theory" are quite relevant to Software Engineering and should be considered as basic science for that field. Numerous illustrations are included.},
keywords = {software engineering},
pubstate = {published},
tppubtype = {techreport}
}