Leveraging Applications of Formal Methods, Verification and Validation. Modeling

The article provides an introduction to the track: Towards a Unified View of Modeling and Programming, organized by the authors of this paper as part of ISoLA 2018: the 8th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation. A total of 19 researchers presented their views on the two questions: what are the commonalities between modeling and programming languages?, and should we strive towards a unified view of modeling and programming? The idea behind the track, which is a continuation of a similar track at ISoLA 2016, emerged as a result of experiences gathered in the three fields: formal methods, model-based software engineering, and programming languages, and from the observation that these technologies share a large common part, to the extent where one may ask, does the following equation hold: $$ modeling = programming $$

In computer science “model” is used with different meanings: Analytic. Analogous field: physics. Relevant “model” meaning: a theory to explain observed natural phenomena. Important: adequacy of the explanations; reproducibility by other researchers of results and experiments. Synthetic. Analogous fields: computer science and engineering. Relevant use of “model”: a constructed artefact (software, hardware,...) built to satisfy a problem specification. Important: the reliability of the constructed artefact; and the correctness of the artefact with respect to the specification. Mechanisation of established hand procedures. Analogous fields: data processing; automation of hospital procedures. (Academically inelegant, but a large percentage of worldwide computer science expenditures.) Relevant: predictability, completeness, reliability, degree of automation, common sense. All three are defensible and productive, but lead to very different ways of thinking. We focus on the analytic and synthetic meanings, since the mechanisation dimension is out of Isola scope.

Modeling languages (like UML and SysML) are those used in model-based specification of software-intensive systems. Like programming languages, they are defined using their syntax and semantics. However, both kinds of languages are defined by different communities, and in response to different requirements, which makes their methodologies and tools different. In this paper, we highlight the main differences between the definition methodologies of modeling and programming languages. We also discuss the impact of these differences on language tool support. We illustrate our ideas using examples from known programming and modeling languages. We also present a case study, where we analyze the definition of a new modeling language called the Ontology Modeling Language (OML). We highlight the requirements that have driven OML definition and explain how they are different from those driving typical programming languages. Finally, we discuss how these differences are being abstracted away using new language definition tools.

The languages used to express specifications, models and programs have much in common. However, in this paper we argue that because they serve different purposes, real care should be taken to distinguish them during development. Rather than seeking unification at the language level, we would recommend exploiting intersections between them where they arise. The main contribution of this paper is to point out the necessary differences and to offer evidence of situations in which common ground can be reached.

We describe the synergies gained by enabling variants for product lines, or features, to be modeled in the same master syntax as design models (class diagrams, state diagrams, composite structure) and traditional source code. Our approach, using a construct we call mixsets, facilitates better analysis, documentation generation, diagram generation, reviewing and testing. It also solves problems related to tool dependency. We have implemented the approach in Umple, building on our previous work which merged design models with code. Our approach continues to allow multiple programming languages to be embedded and generated from the design models. Our extensions allow multiple approaches to separation of concerns (variants, traits, mixins, aspects) to co-exist, operating on models as well as code, and to synergistically enhance each other.

The development of code for software intensive systems involves numerous levels of abstraction, leading from requirements to code. Having abstract modeling concepts available as high-level programming constructs helps to define the code and to make sure that when the system runs with the software executed by machines, the software components behave in the expected way. We explain in this paper that nevertheless, there remains a gap, which cannot be closed by mere programming methods, but which can be closed if programming is supported by an appropriate modeling framework (a design and analysis method and a language).

Despite the substantial progress in the area of deductive program verification over the last years, it still remains a challenge to use deductive verification on large-scale industrial applications. In this abstract, I analyse why this is case, and I argue that in order to solve this, we need to soften the border between models and code. This has two important advantages: (1) it would make it easier to reason about high-level behaviour of programs, using deductive verification, and (2) it would allow to reason about incomplete applications during the development process. I discuss how the first steps towards this goal are supported by verification techniques within the VerCors project, and I will sketch the future steps that are necessary to realise this goal.

In the context provided by the proceedings of the UVMP track of ISoLA 2016, we propose Type Theory as a suitable framework for both modelling and programming. We show that it fits most of the requirements put forward on such frameworks by Broy et al. and discuss some of the objections that can be raised against it.

The language Cogent allows low-level operating system components to be modelled as pure mathematical functions operating on algebraic data types, which makes it highly suitable for verification in an interactive theorem prover. Furthermore, the Cogent compiler translates these models into imperative C programs, and provides a proof that this compilation is a refinement of the functional model. There remains a gap, however, between the C data structures used in the operating system, and the algebraic data types used by Cogent. This forces the programmer to write a large amount of boilerplate marshalling code to connect the two, which can lead to a significant runtime performance overhead due to excessive copying.In this paper, we outline our design for a data description language and data refinement framework, called Dargent, which provides the programmer with a means to specify how Cogent represents its algebraic data types. From this specification, the compiler can then generate the C code which manipulates the C data structures directly. Once fully realised, this extension will enable more code to be automatically verified by Cogent, smoother interoperability with C, and substantially improved performance of the generated code.

This paper considers the relationship between modeling and programming in the context of embedded-software development. In this domain, design and development techniques such as model-based development and model-driven design are often used to improve the efficiency with which software is produced and to broaden the class of engineers who can develop it. This has led some to suggest that modeling has become, or is becoming, programming. The argument advanced in this paper is that the converse is in fact true: programming should rather be considered a form of modeling, with the programming language constituting an executable metalanguage in which models of dynamical systems are encoded and simulated, or “run”. Modeling instead plays a design role, with some models used as a basis for the generation of code, although this is not a requirement: models for which code cannot be generated still play a valuable role in design processes. The basis for this perspective is presented, and research questions based on this viewpoint are given.

The specification of a programming language is a special case of the specification of software in general. This paper discusses the relation between semantics and implementation, or specification and program, using two very different languages for illustration. First, we consider small fragments of a specification of preliminary Ada, and show that what was considered a specification in VDM in 1980 now looks much like an implementation in a functional language. Also, we discuss how a formal specification may be valuable even though seen from a purely formal point of view it is flawed. Second, we consider the simple language of spreadsheet formulas and give a complete specification. We show that nondeterminism in the specification may reflect run-time nondeterminism, but also underspecification, that is, implementation-time design choices. Although specification nondeterminism may appear at different binding-times there is no conventional way to distinguish these. We also consider a cost semantics and find that the specification may need to contain some “artificial” nondeterminism for underspecification.

The activities and the associated formalisms for modeling and programming have many commonalities. In this paper we emphasize this point of view by modeling two examples in the programming language Scala, which have previously been modeled in the VDM specification language, and the Promela modeling language of the SPIN model checker respectively. The latter Scala model uses an internal DSL for hierarchical state machines, and a simple randomized testing framework exposing the same errors as found with SPIN. We believe, as the examples illustrate, that this use of a modern programming language for modeling is promising, especially if utilizing internal DSLs.

SIMULA and Beta are object-oriented languages intended for modeling and programming. This is in contrast to mainstream where different languages are used for modeling and programming. In previous papers, it has been argued that there are a number of advantages in developing a unified language. In order to do this, a consistent terminology for modeling and programming is needed. The notion of model is essential in this respect. In UML, the diagrams are considered models. For SIMULA and Beta the program executions are considered models. We argue for the latter and discuss the implications for the design of a unified language.

Developing and assuring safety- and security-critical real-time embedded systems is a challenging endeavor that requires many activities applied at multiple levels of abstraction. For these activities to be effective and trustworthy, they must be grounded in a common understanding of the system architecture and behavior.We believe that these activities are best addressed in a unified framework of modeling and programming that enables developers, analysts, and auditors to freely move up and down layers of abstraction, shifting their viewpoints to suit the activities at hand, while maintaining strong traceability across the different layers and views. In this approach, the distinction between “models”, “specifications”, and “programs” is often blurred.In this paper, we summarize an architecture-centric approach to critical system development and assurance that emphasizes the use of formally specified architectures as the “scaffolding” through which many different activities are organized and synchronized. We provide examples of: (a) analyses, behavioral constraints, and implementations, (b) important abstraction transitions, and (c) key traceability relationships within the framework. We discuss how these features are being used to develop systems on time and space partitioned execution and communication platforms for systems in the medical domain. We use an open-source medical device that we are developing – Patient-Controlled Analgesic (PCA) infusion pump as a concrete example.

A chain of model-to-model transformations prescribes a particular work process, while executing such a chain generates a concrete instance of this process. Modeling the entire development process itself on a meta-model level extends the possibilities of the model-based approach to guide the developer. Besides refining tools for model creation, this kind of meta-modeling also facilitates debugging, optimization, and prototyping of new compilations. A compiler is such a process system. In this paper, we share the experiences gathered while we worked on the model-based reference compiler of the kieler SCCharts project and ideas towards a unified view on similar prescribed processes.

Computational Thinking has advocated for a decade the importance of a kind of education that elicits and fosters the understanding of computational concepts that are deemed “natural”, thus widely learnable and adoptable, but not supported or at least not explicitly featured nor named in traditional education.In this paper we argue that the most important aspect of this educational revolution is actually the “doing” part, in terms of creating a habit of designing the logic of any project or endeavour in terms of simple models. Simple models, especially if formally underpinned, analyzable, executable, and amenable to code generation for the orchestration of services, are the missing link between computational thoughts and the programming level.Our approach is based on years of experience with middle and high school students, beginner students in Computer Science aged from 17 to over 50, and with students of other disciplines. They have been introduced successfully to CS or programming via constructing simple, yet executable models in the form of short courses, bootcamps, and semester-long courses in various locations and settings.We are convinced that, unlike the widespread push towards coding, this approach is scalable. We also advocate its adequacy to provide the general public of professionals with the kind of familiarity with computational concepts and the level of confidence in practical making of applications and designs that can be a game changer for the societal diffusion of basic computing-related comprehension and design skills.

With the increased demand for so-called “smart” systems, which are required to interact with the physical world in ever more complex ways, we are witnessing a corresponding growth in the complexity of the software that is at the core of such systems. Keeping pace with this rise in complexity is proving to be a challenge for current mainstream programming technologies, whose origins are typically rooted in increasingly outdated computing paradigms that can be traced to some of the earliest applications of computers (e.g., solving numerical problems). This paper first examines some of the salient shortcomings of current mainstream programming technologies; shortcomings that render them unsuitable for addressing modern software applications. This is followed by a discussion of emerging and necessary trends in computer language development, which point to a brand new generation of languages, called design languages. The primary technical requirements for these new languages are identified, and certain pragmatic and socio-economic issues associated with their introduction into industrial practice are reviewed. The paper concludes with a high-level summary of crucial research topics required to realize the full potential of these languages.

Modeling is a fundamental, analytical tool for engineering design. Programming is the synthesis (i.e. construction) of ‘machines’ that do something useful. Advances made during the past three decades showed how these activities are intertwined in systems development and cannot be separated. Arguably, the future of engineered systems shall encompass both, especially considering the design of cyber-physical systems where the computational is in continuous interaction with the physical. State-of-the-art industrial practice appears to focus on ‘model-based programming’ – programming with higher-level abstractions. In this paper we outline a broader picture for integrating modeling and programming, and what it means for engineering processes and engineering education.

Modeling in general is of course different from programming (think: climate models). However, when we consider the role of models in the context of “model-driven”, i.e., when they are used to automatically construct software, it is much less clear that modeling is different from programming. In this paper, I argue that the two are conceptually indistinguishable, even though in practice they traditionally emphasize different aspects of the (conceptually indistinguishable) common approach. The paper discusses and illustrates language-oriented programming, the approach to {modeling|programming} we have successfully used over the last 7 years to build a range of innovative systems in domains such as insurance, healthcare, tax, engineering and consumer electronics. It relies on domain-specific languages, modular language extension, mixed notations, and in particular, the Jetbrains MPS language workbench.

The paper considers domain-specific tool support as a means to turn descriptive into prescriptive models, and to blur the difference between models and programs, and even between developers and users. Conceptual underlying key is to view the system development as a decision process which increasingly constraints the range of possible system implementations and Domain-Specific Languages (DSLs) as a means to freeze taken decisions on the way towards a concrete realization. This way naturally comprises both programming and modeling aspects. In fact, considering all interactions that influence the behaviour of the system as development turns GUIs into DSLs and makes it even hardly possible to draw the line between developers and users. We will illustrate this viewpoint in the light of the development of the Equinocs system, Springer’s new editorial service.

After decades of progress on Correctness-by-Construction (CbC) as a scientific discipline of engineering, it is time to look further than correctness and investigate a move from CbC to XbC, i.e., considering also non-functional properties. X-by-Construction (XbC) is concerned with a step-wise refinement process from specification to code that automatically generates software (system) implementations that by construction satisfy specific non-functional properties concerning security, dependability, reliability or resource/energy consumption, to name but a few. This track brings together researchers and practitioners that are interested in CbC and the promise of XbC.

Deductive program verification can be used effectively to verify high-level programs, but can be challenging for low-level, high-performance code. In this paper, we argue that compilation and program transformations should be made annotation-aware, i.e. during compilation and program transformation, not only the code should be changed, but also the corresponding annotations. As a result, if the original high-level program could be verified, also the resulting low-level program can be verified. We illustrate this approach on a concrete case, where loop annotations that capture possible loop parallelisations are translated into specifications of an OpenCL kernel that corresponds to the parallel loop. We also sketch how several commonly used OpenCL kernel transformations can be adapted to also transform the corresponding program annotations. Finally, we conclude the paper with a list of research challenges that need to be addressed to further develop this approach.

In this paper we sketch a transformation-oriented framework for establishing system characteristics like model-checkability, learnability, or performance. Backbone of our framework is Cinco, our meta tooling suite for generating DSL-specific development environments on the basis of specifications in terms of metamodels. Cinco is used here to specify the considered source and target languages, as well as the transformation language that allows one to transform source systems/models into semantically equivalent, X-conform target systems. In this paper, we focus on illustrating the power of domain-specific transformation languages by presenting a multi-level transformation pattern that allows one to elegantly capture refinement and aggregation aspects in a rule-based fashion. All this is explained along a number of examples.

Patterns have greatly improved the development of programs and software by identifying practices that could be replayed and reused in different software projects. Moreover, they help to communicate new and robust solutions for software development; it is clear that design patterns are a set of recipes that are improving the production of software. When developing models of systems, we are waiting for adequate patterns for building models and later for translating models into programs or even software. In this paper, we review several patterns that we have used and identified, when teaching and when developing case studies using the Event-B modelling language. The modelling process includes the use of formal techniques and the use of refinement, a key notion for managing abstractions and complexity of proofs. We have classified patterns in classes called paradigms and we illustrate three paradigms: the inductive paradigm, the call-as-event paradigm and the service-as-event paradigm. Several case studies are given for illustrating our methodology.

Formal verification of compiler correctness requires substantial effort. A particular challenge is lack of modularity and automation. Any change or update to the compiler can render existing proofs obsolete and cause considerable manual proof effort. We propose a framework for automatically proving the correctness of compilation rules based on simultaneous symbolic execution for the source and target language. The correctness of the whole system follows from the correctness of each compilation rule. To support a new source or target language it is sufficient to formalize that language in terms of symbolic execution, while the corresponding formalization of its counterpart can be re-used. The correctness of translation rules can be checked automatically. Our approach is based on a reduction of correctness assertions to formulas in a program logic capable of symbolic execution of abstract programs. We instantiate the framework for compilation from Java to LLVM IR and provide a symbolic execution system for a subset of LLVM IR.

In stepwise program development, abstract specifications can be transformed into (parallel) programs which preserve functional correctness. Although tackling bad performance after a program’s deployment may require a costly redesign, deployment decisions are usually made very late in program development. This paper argues for the introduction of deployment decisions as an integrated part of a development-by-construction process: Deployment decisions should be expressed as part of a program’s high-level model and evaluated by how they affect program performance, using metrics at an appropriate level of abstraction. To illustrate such a deployment-by-construction process, we sketch how deployment decisions may be modelled and evaluated, concerning data layout in shared memory for parallel programs targeting shared-memory multicore architectures with caches. For simplicity, we use an abstract metric of data access penalties and simulate data accesses on a memory system which internally ensures data coherency between cores.

Performance is an important extra-functional factor that directly impacts on the quality of a software system as perceived by its users. It indicates how well the software behaves, thus complementing functional properties that concern what the software does. Its ever-increasing relevance cannot be underestimated.

Finding suitable ways to handle personal data in conformance with the law is challenging. The European General Data Protection Regulation (GDPR), enforced since May 2018, makes it mandatory to citizens and companies to comply with the privacy requirements set in the regulation. For existing systems the challenge is to be able to show evidence that they are already complying with the GDPR, or otherwise to work towards compliance by modifying their systems and procedures, or alternatively reprogramming their systems in order to pass the eventual controls. For those starting new projects the advice is to take privacy into consideration since the very beginning, already at design time. This has been known as Privacy by Design (PbD). The main question is how much privacy can you effectively achieve by using PbD, and in particular whether it is possible to achieve Privacy by Construction. In this paper I give my personal opinion on issues related to the ambition of achieving Privacy by Construction.

Correctness-by-Construction (C-by-C) approaches software development as formal engineering and builds correct code by iterating from a correct specification. However, C-by-C is focused on functional properties of the system. X-by-Construction (X-by-C) extends C-by-C to also consider non-function properties concerning aspects such as security, dependability, reliability or energy consumption. In this work we consider the challenges of applying X-by-C to non-functional security properties such as side-channel attacks. We demonstrate how such non-functional security can be captured and reasoned about in an X-by-C manner, yielding the benefit of C-by-C for non-functional properties and security challenges.

Guaranteeing that information processed in computing systems remains confidential is vital for many software applications. To this end, language-based security mechanisms enforce fine-grained access control policies for program variables to prevent secret information from leaking through unauthorized access. However, approaches for language-based security by information flow control mostly work post-hoc, classifying programs into whether they comply with information flow policies or not after the program has been constructed. Means for constructing programs that satisfy given information flow control policies are still missing. Following the correctness-by-construction approach, we propose a development method for specifying information flow policies first and constructing programs satisfying these policies subsequently. We replace functional pre- and postcondition specifications with confidentiality properties and define rules to derive new confidentiality specifications for each refining program construct. We discuss possible extensions including initial ideas for tool support. Applying correctness-by-construction techniques to confidentiality properties constitutes a first step towards security-by-construction.

We present a tutorial introduction to the usage of Cinco, our framework for the generation of graphical development environments, highlighting two recent additions: the possibility to bringing any Cinco-based graphical modeling language into the web, and a graphical editor for meta modeling. All the discussed features are illustrated step by step along the development and evolution of the WebStory, a simple education-oriented modeling language for adventure games.

Low cost embedded cyber-physical systems and ubiquitous networking have opened up a new world of connected devices in our homes and workplaces, and in safety critical contexts such as automobiles, medical care, and drone-based air vehicles. There are many different approaches to developing and assuring these systems, but not all take a rigorous approach and even fewer offer integrated assurance frameworks.In this STRESS 2018 tutorial, we introduce students to an integrated modeling and verification environment for high-assurance embedded systems based on the Sireum translation, analysis, and verification platform from Kansas State University. Sireum includes a programming language called Slang for developing high-assurance embedded applications and a verification framework called Logika that uses symbolic execution technology to provide highly automated and easy-to-use software contract checking capabilities. Slang and Logika align with the Architecture and Analysis Definition Language (AADL) for architecture modeling and component interface declarations, analysis of AADL models, and configuration of execution platforms using standard AADL properties. AADL component behavioral properties can be specified and verified using, for example, the Behavioral Language for Embedded Systems with Software (BLESS).

Language-Driven Engineering (LDE) is a new paradigm that aims at involving stakeholders, including the application experts, in the system development and evolution process using dedicated domains-specific languages (DSLs) tailored to match the stakeholders’ mindsets. The interplay between the involved DSLs is realized in a service-oriented fashion, with corresponding Mindset-Supporting Integrated Development Environments (mIDEs). This organization eases product line and system evolution, because one can introduce and exchange entire DSLs as if they were services. Using as example a smart email classification system that highlights important emails in the inbox, we model its decision procedure in a tailored graphical domain-specific language based on Binary Decision Diagrams. BDDs are a compact form of the popular decision trees and thus a mindset natural to many application experts. We then evolve this language and its mIDE to meet the new users’ wish to model some uncertainty in the classification. To evolve the language, we first manually adapt its metamodel and code generator. Subsequently we show, how this step can be automated by refining the BDD DSL with a dedicated DSL for defining algebraic structures. As this exchange happens in a service-oriented fashion, it does not impair the optimization potential and nicely follows the successive refinement of the users’ mindset.

This tutorial presents and motivates various malware detection tools and illustrates their usage on a clear example. We demonstrate how statically-extracted syntactic signatures can be used for quickly detecting simple variants of malware. Since such signatures can easily be obfuscated, we also present dynamically-extracted behavioral signatures which are obtained by running the malware in an isolated environment known as a sandbox. However, some malware can use sandbox detection to detect that they run in such an environment and so avoid exhibiting their malicious behavior. To counteract sandbox detection, we present concolic execution that can explore several paths of a binary. We conclude by showing how opaque predicates and JIT can be used to hinder concolic execution.