Home McSCert Seminars
McSCert Seminars
Title Model Management with Epsilon
Presenter Richard Paige
Date Monday April 8, 2013  at 1:30 pm
Abstract This talk will give an overview of the Epsilon model management framework and some of its recent applications. It will present the conceptual architecture of Epsilon (and its motivation) as well as a selection of the tasks that it currently supports. Industrial applications from a variety of domains - safety, real-time, business analytics/big data - will be introduced.
iography

Richard Paige is Professor of Enterprise Systems in the Department of Computer Science, University of York, UK. He leads the Enterprise Systems group (around 30 researchers and academics) which focuses on the theory, practice and socio-technical applications of Model-Driven Engineering. He received his PhD from the University of Toronto in 1997, and now speaks almost fluent Yorkshire.


Refreshments will be served

   
Title Embedded Systems as Programs and Standards as Validation
Presenter Edward Griffor
Date 20 September 2012
Abstract

Certification of SW to a standard should include a conceptual framework of SW attributes, relating to ‘safe’ behavior of that SW in the intended environment, and feasible methods for demonstrating those attributes. The constraints expressed in the language of those attributes should capture the logical, methodological or empirical discipline used to develop the SW. The logical refers to the structure or construction of the program (type theoretic or logical approaches). The methodological refers to the program having been developed using a standardized processes and the empirical refers to the discipline of assessing the performance of SW with respect to standardized metrics.

 

All of these disciplines, and frequently combinations of more than one, are meant to provide a level of confidence that the SW developed will behave/perform ‘as intended in the intended environment’, i.e., as a form of SW validation. As a source of some of the most complex (by simplistic measures such as LOC or cyclomatic complexity) and some of the most broadly deployed embedded SW systems, the automotive industry faces today critical certification challenges in this sense. Their certification challenges are complicated by the vast number of variants of each such system produce, each one a ‘carrier’ for the ever more complex functions, and the non-linear architecture that results from a ‘use-based’ approach to I/O – this suggests the need for emphasis on ‘Architecture for Certification’.

 

I will review the Advanced Industry Strategies in approaching the architecture for today’s automotive Cyber Physical Systems with examples from powertrain, body and safety electronics and suggest several research questions.

Biography

Dr. Edward Griffor is one of the three existing Walter P. Chrysler Technical Fellows, one of the highest technical positions in industry and one that represents technical excellence throughout global industry, from the automotive to the aerospace, medical and computing industries. He is the Chairman of The MIT Alliance, a professional association of scientists, engineers, and business experts trained at the Massachusetts Institute of Technology. Dr. Griffor completed his doctoral studies, in Mathematics and Electrical Engineering, at MIT in 1980 and was NSF-NATO Postdoctoral Fellow in Science and Engineering at the University of Oslo in Norway from 1980-83. He later held faculty positions at the University of Oslo in Norway, Uppsala University in Sweden, the Catholic University of Santiago in Chile and other universities in Europe and the Americas as well as having lectured at Harvard University, MIT and Tufts University in the U.S. Dr. Griffor is regarded as a world expert in the use of mathematical methods for developing electronics for controls and Embedded SW Engineering as well as in computation for Cyber Physical Systems. In addition to his technical leadership position at Chrysler Group LLC, Dr. Griffor is Adjunct Professor at the Center for Molecular Medicine and Genetics of Wayne State University School of Medicine in Detroit, MI. He is a member of the Board of Directors of MCASTL, the US Department of Transportation funded Michigan Center for Advancing Safe Transportation throughout the Lifespan at the University of Michigan, and of the Board of Directors of the VIIC (US Department of Transportation and US Federal Highway funded Vehicle Infrastructure Integration Consortium) and sits on the Board of Directors of the MITEF (Massachusetts Institute of Technology Enterprise Forum). Dr. Griffor and his wife, Hon. Mariela Griffor Consul of Chile in Michigan, live with their two daughters in Grosse Pointe Park, MI USA.

Slides  

 

 

 

 

Title Assurance Case Research - Themes and Current Directions
Presenter Tim Kelly, University of York, UK
Date 3 July 2012
Abstract The concept of safety case development and acceptance has been around for many decades - originating from the UK Civil Nuclear Industry in the 1960s.  The research and practice of using structured argumentation notations and techniques has also been in existence for a significant period of time (approaching twenty years).   In this talk I will provide a tour of the development of research in this area over this period up to the present day, with the aim of highlighting core themes and directions.  This will describe past work on safety case patterns, modular certification, software safety cases, dealing with confidence, and the generalisation of safety case practice to other disciplines such as security.   The description of current research will describe joint work between the universities of York and Virginia on Assured Argument Development (recently promoted by the US FDA) - which formed part of our response to the findings of the publicly-funded UK review into the issues surrounding the explosion of the XV230 Nimrod aircraft in Afghanistan.  Finally,  an overview will be given of a recently commenced EU FP7 project - OPENCOSS (Open Platform for Evolutionary Certification of Open Systems).
Biography Dr Kelly is a Senior Lecturer within the Department of Computer Science at the University of York. He is perhaps best known for his work on system and software safety case development, particularly his work on refining and extending the Goal Structuring Notation (GSN). His research interests include safety case management, software safety analysis and justification, software architecture safety, certification of adaptive and learning systems, and the dependability of “Systems of Systems”. He has supervised a number of research projects in these areas with funding and support from Airbus, BAE SYSTEMS, Data Systems and Solutions, DTI, EPSRC, ERA Technology, Ministry of Defence, QinetiQ and Rolls-Royce. He has published over 150 papers on high integrity systems development and justification in international journals and conferences. He is also Managing Director of Origin Consulting (York) Limited – a consultancy company specialising in safety critical systems development and assurance.
Slides pdf

 

Title Systems and Software Engineering Standards for the Medical Domain
Presenter Vera Pantelic
Date 24 April 2012
Abstract In this talk, some concepts important in the field of safety-critical software-intensive systems are surveyed as defined and used in relevant systems and software engineering standards in the medical domain. The focus is on two standards: IEC 62304 (the main software standard in the medical domain), and IEC 61508 (a generic safety standard intended as a guidance for different domains). The considered concepts include safety integrity levels, process vs. product requirements, and assurance cases.
Biography Vera Pantelic is currently working as a postdoctoral fellow with the McMaster Centre for Software Certification (McSCert). She received both her M.A.Sc. and Ph.D. in Software Engineering from McMaster University. Her main research interests include supervisory control of discrete event systems, and verification and certification of safety-critical software-intensive systems.
Slides pdf

 

Title

Uncertainty Quantification and the PSUADE software
Presenter Mahmoud Khademi
Date 23 March 2012
Abstract Uncertainty quantification (UQ) is the science of quantitative characterization and reduction of uncertainties in applications. It tries to resolve how probable particular outcomes are, if some aspects of the system are not precisely known. UQ is defined as the identification (sources of uncertainties), characterization (types of uncertainties), propagation during the simulation, analysis (uncertainty impacts), and reduction of uncertainties in simulation models.

In this talk, we discuss general methods and algorithms for uncertainty quantification and statistical modeling of complex systems such as Markov chain Monte Carlo, polynomial regression, multivariate adaptive regression splines, Bayesian computation and machine learning techniques for decision making and non-linear dimensionality reduction. We overview the capabilities of PSUADE (Problem Solving environment for Uncertainty Analysis and Design Exploration, https://computation.llnl.gov/casc/uncertainty_quantification/), which is a software toolkit for UQPSUADE has a valuable set of tools for accomplishing uncertainty analysis, global sensitivity analysis, design optimization, model calibration, etc.
Biography Mahmoud Khademi is an M.Sc. student in the Department of Computing and Software.
Slides ppt

 

Title

Logical Analysis of Hybrid Systems:  Proving Theorems for Complex Dynamics
Presenter André Platzer
Date 15 March 2012
Abstract

Hybrid systems model cyber-physical systems as dynamical systems with interacting discrete transitions and continuous evolutions along differential equations.  They arise frequently in many application domains, including aviation, automotive, railway, and robotics.  Because these systems operate in the physical world, stringent safety requirements are usually imposed on cyber-physical system designs.  There is a well-understood theory for guaranteeing correct functioning of computer programs using logic and formal verification techniques.  But what about cyber-physical systems?   How can we ensure that cyber-physical systems are guaranteed to meet their design goals, e.g., that an aircraft cannot crash into another one?

This talk describes how logic and formal verification can be lifted to hybrid systems.  It presents the theoretical and practical foundations of logical analysis of hybrid systems.  The talk describes a logic for hybrid systems called differential dynamic logic and gives a perfectly compositional proof technique.  This logical approach is implemented in the verification tool KeYmaera and has been used used successfully for verifying nontrivial properties of aircraft, railway, and car control applications. The logical approach is also interesting from a theoretical perspective, because it shows how verification techniques for continuous dynamics can be lifted to hybrid systems by a complete axiomatization.

Note also André's related seminar on the previous day.

Biography André Platzer is an Assistant Professor in the Computer Science Department at Carnegie Mellon University. His interests include logical foundations of cyber-physical systems, hybrid systems, distributed hybrid systems, stochastic hybrid systems, logic in computer science, automated theorem proving, model checking, symbolic and numerical computation.

André has developed theory, practice, and applications of logical analysis and verification of hybrid systems, and he proved the very first completeness theorem for hybrid systems. He introduced compositional verification techniques and methods that can verify hybrid systems without solving their differential equations (called differential invariants). In addition, he led the development of the first theorem prover for hybrid systems (KeYmaera) and he has worked on verification of aircraft, railway, and car control systems.

André Platzer also introduced the first formal verification approach for distributed hybrid systems, in which participants can appear and disappear dynamically while the system follows its hybrid dynamics.
Slides pdf

 

Title

Toward a Driver's License Test for Robotic Cars: How to Prove Your Car Correct
Presenter André Platzer
Date 14 March 2012
Abstract

Car safety measures can be most effective when the cars on a street coordinate their control actions using distributed cooperative control. While each car optimizes its navigation planning locally to ensure the driver reaches his destination, all cars coordinate their actions in a distributed way in order to minimize the risk of safety hazards and collisions. These systems control the physical aspects of car movement using cyber technologies like local and remote sensor data and distributed V2V and V2I communication. They are thus cyber-physical systems. In this talk, we consider a distributed car control system that is inspired by the ambitions of the California PATH project, the CICAS system, SAFESPOT and PReVENT initiatives. We develop a formal model of a distributed car control system in which every car is controlled by adaptive cruise control. One of the major technical difficulties is that faithful models of distributed car control have both distributed systems and hybrid systems dynamics. They form distributed hybrid systems, which makes them very challenging for verification. In a formal proof system, we verify that the control model satisfies its main safety objective and guarantees collision freedom for arbitrarily many cars driving on a street, even if new cars enter the lane from on-ramps or multi-lane streets. The model we present is in many ways one of the most complicated cyber-physical systems that has ever been fully verified formally. In this talk, we also illustrate how controllers for intersection collision coordination scenarios can be verified. Finally, we develop formal models for cyber-physical systems style freeway traffic scenarios and verify an intelligent speed adaptation model that respects variable speed limit control and incident management. While this talk will focus mostly on the application context of car control and how formal verification can achieve our "driver's license test for robotic cars", we will provide some background on the underlying verification technology for differential dynamic logic implemented in the verification tool KeYmaera. This is joint work with Sarah Loos, Ligia Nistor, and Stefan Mitsch.

Technically this seminar was for the Computing and Software Department rather than McSCert, but is included because of its close connection with the McSCert seminar on the following day.

Biography André Platzer is an Assistant Professor in the Computer Science Department at Carnegie Mellon University. His interests include logical foundations of cyber-physical systems, hybrid systems, distributed hybrid systems, stochastic hybrid systems, logic in computer science, automated theorem proving, model checking, symbolic and numerical computation.

André has developed theory, practice, and applications of logical analysis and verification of hybrid systems, and he proved the very first completeness theorem for hybrid systems. He introduced compositional verification techniques and methods that can verify hybrid systems without solving their differential equations (called differential invariants). In addition, he led the development of the first theorem prover for hybrid systems (KeYmaera) and he has worked on verification of aircraft, railway, and car control systems.

André Platzer also introduced the first formal verification approach for distributed hybrid systems, in which participants can appear and disappear dynamically while the system follows its hybrid dynamics.
Slides pdf

 

Title Nix and its Potential Role in Configuration Management
Presenter Russell O'Connor
Date 14 November 2011
Abstract Nix is a "purely functional" package manager meaning that the software it manages is purely a function of its build specification and does not depend on the state of the build system.  Each software package built by Nix lives in a unique store location such as:

/nix/store/r8vvq9kq18pz08v249h8my6r9vs7s0n3-firefox-2.0.0.1/

where r8vvq9kq… is a cryptographic hash of the package's build dependency graph which uniquely identifies the package.  Nix's approach to package management enables many powerful features such as:

- allowing multiple conflicting versions of packages to coexist
- ensuring complete dependencies of packages have been specified
- allowing atomic upgrades and rollbacks of installed packages
- creating package dependency closures for distribution
- transparent source/binary deployment and binary patching
- service deployment

NixOS is an entire Linux distribution that not only relies on Nix for package management, but also uses Nix for system configuration.

Although Nix was not designed for safety-critical configuration management, I believe that Nix's ability to capture and completely identify software dependencies could be a powerful tool for configuration management of safety-critical software.

In this talk I will give an overview of how Nix was designed to work and then review the unqiue features of Nix that could be applied to the problem of configuration management and software deployment.

Nix was developed at Utrecht University by Eelco Dolstra et al.  I have been using NixOS as my primary Linux distribution for two years.  For more information about Nix see http://nixos.org.
Biography  Russell O'Connor obtained a bachelor's degree in pure mathematics and computer science from the University of Waterloo.  He was awarded a PhD 'cum laude' from Radboud University Nijmegen in the Foundations Group for his work on efficient computer verified exact real arithmetic.  He now holds a post-doctoral position at McMaster University's department of Computing and Software working on the MathScheme system as part of the Software Certification project.
Slides pdf (originally produced by Ludovic Courtes and Eelco Dolstra)

 

Title Safety Assurance Cases
Presenter Zarrin Langari
Date 27 July 2011
Abstract In this talk, I give a brief overview on what assurance cases are, and mainly give a summary of the previous seminar on assurance cases by Marc Bender. The focus of my talk is on how to build a safety assurance case through a simple example. I present the main elements of safety arguments as it is shown by Goal Structuring Notation.  Also, in a step-by-step approach, I  show how to use these elements in building a safety assurance case for a simple example.
 
Biography Zarrin Langari is a postdoc fellow with the McMaster Centre for Software Certification (McSCert).  She obtained her Ph.D in computer science from University of Waterloo  in 2010 under the supervision of Richard Trefler. Her research interests include analysis and formal methods for verification of safety-critical software systems, and formal modeling in Model-based Software Engineering. After attending the Professor John Knight's course on Safety Assurance Cases, she became interested in investigating effective model-based methodologies for developing safety cases.    
 
Slides Not available

 

Title What is Software Certification?
Presenter Marc Bender
Date 13 April 2011
Abstract

In software engineering, as in other engineering disciplines, we are faced with the difficult task of trying to quantify quality.  When is a piece of software "acceptable" from an engineering standpoint?  How do we provide a "seal of approval" that indicates that we have deemed it acceptable?  These are some of the questions that are tackled by software certification.  Members of the McMaster Centre for Software Certification (McSCert) have done some excellent work on understanding and answering these questions; the goal of this presentation is to talk about some of this work.

 

This talk is divided into three parts.  First, I will discuss some important ontological issues:  what precisely do we mean by software, certification, quality, acceptability, etc.?  Second, I will consider some practical aspects of certification, such as the parties involved and their various roles and responsibilities.  Finally, I will present a novel dissection of certification into five parts - evidence, confidence, criteria, determination and certificates - and discuss the signification and significance of each.

Biography

Marc Bender is a postdoctoral fellow with the McMaster Centre for Software Certification (McSCert).  He obtained his Ph.D in computer science from McMaster University in 2010 under the supervision of Jeff Zucker.  His research interests include programming language theory, higher-order modal logic, and the philosophical and mathematical foundations of computer science and software engineering.  He currently divides his time between research on the foundations of software certification, collaborative work on software qualification with SWI (one of McSCert's industrial partners), and software consultation and development for Digital Dash Inc.

Slides pdf

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

Title Applying Software Engineering Principles to Computational Science
Presenter Jeff Carver, University of Alabama
Date 7 April 2011
Abstract The increase in the importance of Computational Science software motivates the need to identify and understand which software engineering (SE) practices are appropriate. Because of the uniqueness of the computational science domain, exiting SE tools and techniques developed for the business/IT community are often not efficient or effective. Appropriate SE solutions must account for the salient characteristics of the computational science development environment. To identify these solutions, members of the SE community must interact with members of the computational science community. This presentation will discuss the findings from a series of case studies of CSE projects and the results of an ongoing workshop series. First, a series of case studies of computational science projects were conducted as part of the DARPA High Productivity Computing Systems (HPCS) project. The main goal of these studies was to understand how SE principles were and were not being applied in computational science along with some of the reasons why. The studies resulted in nine lessons learned about computational science software that are important to consider moving forward. Second, the Software Engineering for Computational Science and Engineering workshop brings together software engineers and computational scientists. The outcomes of this workshop series provide interesting insight into potential future trends. The presentation will conclude with a brief overview other software engineering research being performed by faculty at the University of Alabama.
Biography Jeff Carver is an Assistant Professor in the Computer Science Department at the University of Alabama. He earned his PhD in 2003 from the University of Maryland under the direction of Dr. Victor Basili. His main research interests include empirical software engineering, software engineering for computational science, and software quality assurance. He has been studying scientific software development for the past seven years. One of his main goals is to understand how best to apply software engineering principles to the domain of scientific and engineering software development. His early work in this area was conducted as part of the DARPA HPCS project. He is interested in establishing collaborations with interested practitioners in this area.
Slides pdf
Last Updated on Friday, 05 April 2013 15:10