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}
}
2018
Qian, Zhizhao
High-Fidelity Simulation Model of a Dual FIFO CAN Stack Masters Thesis
McMaster University, 2018.
Abstract | Links | BibTeX | Tags: CAN, Controller Area Network, modeling, SimEvents, simulation, timing analysis
@mastersthesis{Qian2018,
title = {High-Fidelity Simulation Model of a Dual FIFO CAN Stack},
author = {Qian, Zhizhao},
url = {https://www.mcscert.ca/qian_zhizhao_201803_masc_software_engineering/},
year = {2018},
date = {2018-05-04},
school = {McMaster University},
abstract = {This thesis presents a simulation model for a Control Area Network (CAN) software stack, the Dual FIFO CAN (DFC) stack, and a method for identifying and incorporating the details of the host environment (hardware setup, operating system, etc.) into the implementation of the simulation model in order to achieve a high level of fidelity. The method enable the simulation model to produce more realistic simulation results that are close to real-life experiments of the target system compared to existing commercial and academic simulation tools, which mostly ignore the system details The simulation model is implemented based on the specification documents of the DFC stack as well as knowledge gained from real-life experiments about the DFC stack and its host environment, a dual-core Electric Control Unit (ECU) hardware test bench that runs a Real-Time Operating System (RTOS). Like the actual DFC stack, the simulation model offers features such as dual non-preemptive FIFO transmit queues and TX buffers, and reserved slots in the queues for higher-priority messages. By using the method introduced in this research, the simulation model also offers options, once enabled and configured with proper parameters, for simulating a host environment that has effects on the behaviors of the modeled CAN stack. And these features are not fully available in existing commercial and academic simulation tools. The model provides internal calibration values of the DFC stack as configurable parameters to the user, making it easy to customize the simulation. Configurable calibration values includes the total number of slots in the transmit FIFO queues, number of reserved slots in the queues, transmit-rate thresholds that decide to which transmit queue a message is routed and whether a message is eligible to enter the reserved slots of the queues, and together they determine the queuing behaviors of the DFC stack. The options for simulating a host environment (an ECU on a CAN network in a modern vehicle, for instance) is capable of recreating the timing effects (delays, jitters or other effects due to the processing load, physical limitation and internal implementation) of the target host environment on the simulation results. Both deterministic (constant values, etc.) and/or statistical (probability distributions, etc.) models can be used to configure each single timing effect from the simulated host environment. The simulation model is also automated to transmit a set of customized transmit message (configurable message ID, DLC, period and internal transmission priority) and process simulation results according to the purpose of the simulation (statistical analysis, plots of data, etc). These features make it possible for the simulation model to be used not only to simulate various customized simulation scenarios, but also for different purposes in various stages of the development process, for instance, a pre-experiment simulation run before a test bench experiment to test the correctness of the calibrations and predict the possible outcomes of the experiment, or, simulations for confirmation purposes in order validate the test bench data after the test experiment. The model is compatible with typical modeling, simulation and development environments as it is implemented in MATLAB SimEvents environment, which works with third-party CAN development tools such as Vector CANoe. It is also designed to work with the high-fidelity model of the Vector CAN protocol stack from Whinton (2016).},
keywords = {CAN, Controller Area Network, modeling, SimEvents, simulation, timing analysis},
pubstate = {published},
tppubtype = {mastersthesis}
}
2015
Whinton, Grant
Higher-Fidelity Modelling and Simulation of the CAN Protocol Stack Masters Thesis
McMaster University, 2015.
Abstract | Links | BibTeX | Tags: CAN, Controller Area Network, modelling, network analysis, SimEvents, simulation
@mastersthesis{Whinton2015,
title = {Higher-Fidelity Modelling and Simulation of the CAN Protocol Stack},
author = {Whinton, Grant},
url = {https://www.mcscert.ca/whinton-grant-masters-2015-e_thesis/},
year = {2015},
date = {2015-09-28},
school = {McMaster University},
abstract = {This thesis details a higher-fidelity, scalable simulation tool and model for message response time and bus utilization rate analysis for the Controller Area Network (CAN) protocol stack. This tool achieves higher fidelity than existing commercial and academic simulation tools by including details of the stack implementation that are often neglected, such as receive and transmit hardware buffer availability and usage policy (i.e., which messages are able to be copied to which buffer resources), and the buffer polling or queueing policies. Key details of these features have been identified by a thorough examination of CAN stack behaviour, taking into account the physical considerations of commercial CAN implementations. Inclusion of these details in the simulation can produce better accuracy by exposing certain priority inversion scenarios. Scalability is achieved by using a transaction-based modelling approach and modelling transmissions at the protocol level rather than the physical/bit level. The tool requires minimal user interaction, and system level model generation is automated using an AUTOSAR XML system description file (ARXML format) to specify network topology and message information (transmitter, receiver(s), period, length, etc.), and an Excel spreadsheet file (XLS or XLSX format) to specify node hardware/software implementation details (buffer resource details, polling loop rates, main control loop rates, etc.) as inputs.},
keywords = {CAN, Controller Area Network, modelling, network analysis, SimEvents, simulation},
pubstate = {published},
tppubtype = {mastersthesis}
}