We describe a novel approach to program verification and its application to verification of C programs, where properties are expressed in matching logic. The general approach is syntax-directed: semantic rules, expressed according to Knuth's attribute ...

Interactive programs, like user interfaces, are hard to formally specify and thus to prove correct. Some ideas coming from functional programming languages have been successful to improve the way we write safer programs, compared to traditional ...

An important and growing class of cyber physical systems are autonomous vehicles (AVs). While the U.S. military has used AVs, such as unmanned air vehicles, for many years, civilian use of these vehicles, e.g., by the FBI, has been steadily increasing. ...

Model-based development (MBD) is increasingly being used to develop embedded control software, with Matlab Simulink/Stateflow being the most widely used MBD language in the automotive industry. Stateflow truth tables, more traditionally known as ...

The engineering of dependable cyber-physical systems (CPSs) is inherently collaborative, demanding cooperation between diverse disciplines. A goal of current research is the development of integrated tool chains for model-based CPS design that support ...

The lightweight use of formal methods is an effective approach to using formal specifications in various phases of software development. This paper proposes tool support specialised for the earlier stages of development that involves incremental and ...

Gene regulatory relationships constitute a complex mechanism of interactions adopted by cells to control behaviours and functions of a living organism. The identification of such relationships from genomics data through a computational approach is a ...

We suggest a method for measuring the degree to which features interact in feature-oriented software development. To this end, we extend the notion of simulation between transition systems to a similarity measure and lift it to compute a behaviour ...

We describe our experiences from using formal verification tools during the standardization process of Dual Connectivity, a new feature in LTE developed by 3GPP. To the best of our knowledge, this is the first report of its kind in the telecom industry. ...

This paper discusses the use of test and animation techniques to validate an access control policy, expressed in SecureUML. It reports on a case study of secure medical information system, where the SecureUML model expresses both functional and security ...

Formal methods have been "preached" as a means to achieve better reliability and other qualities in software and systems for half a century. Despite many success stories confirmed their effectiveness, there is still much reluctance (not only) in the ...