HILT 2013             ACM logo - Advancing Computing as a Science & Profession

High Integrity Language Technology
ACM SIGAda’s Annual International Conference

Sunday Morning Tutorials (9:00am - 12:30pm)

SA1: Object-Oriented Programming in Ada 2012, Part 1
Ed Colbert (Absolute Software)

Audience and Prerequisites: Ada programmers, designers, and reviewers. Understanding of OO concepts and Ada 83.

Ada 05 makes it easier to learn and use object-oriented programming (OOP) than Ada 95, as well integrating OOP with concurrent programming. Ada 2012 makes small changes to the OOP model of Ada 05's that facilitate its use, and that make it easier for the compiler to detect errors. Ada 2012 also adds contracts that allow the OO programmer to define the perceived behavior of a tagged type and at the same time constrain the behavior of derived types.

(Note: if you attended last year's tutorial, you'll want to attend Part 2, which covers the material we didn't have time for. If you can't attended this year's tutorial, he will send you the full revised presentation.)

SA2: Proving Safety of Parallel / Multi-Threaded Programs
Tucker Taft (AdaCore)

This tutorial will introduce the attendees to analysis and proof techniques for programs using parallelism and multi-threading. There are no specific prerequisites, but a familiarity with the notions of preconditions and postconditions, aliasing, race conditions, and deadlocks would be of value. The examples will be based on the threading and parallelism models of Java, Ada, and two new parallel languages, one called ParaSail and another, inspired by the verifiable SPARK subset of Ada, called Sparkel. We will introduce the distinction between safety and liveness properties, and then focus primarily on techniques for the verification of safety properties, including the absence of race conditions and deadlocks. Both lock-based and lock-free synchronization approaches will be considered. We will also discuss the issue of determinism vs. non-determinism in parallel and multi-threaded programs.

Sunday Afternoon Tutorials (2:00 - 5:30pm)

SP1: Object-Oriented Programming in Ada 2012, Part 2
Ed Colbert (Absolute Software)

Audience and Prerequisites: Ada programmers, designers, and reviewers. Understanding of Ada 95's OO Support (see tutorial SA1).

See Part 1 (Tutorial SA1) for general description. The topics covered in Part 2 are

(Note: if you attended last year's tutorial, you'll want to attend Part 2, which covers the material we didn't have time for. If you can't attended this year's tutorial, he will send you the full revised presentation.)

SP2: Engineering Domain-Specific Languages with FORMULA 2.0
Ethan K. Jackson (Microsoft Research)

Audience and Prerequisites: Those interested in formal specifications and formal methods for practical use in industrial projects.

Domain-specific languages (DSLs) are useful for capturing and reusing engineering expertise. They can formalize industrial patterns and practices while increasing the scalability of verification, because input programs are written at a higher level of abstraction. However, engineering new DSLs with custom verification is a non-trivial task in its own right, and usually requires programming language, formal methods, and automated theorem proving expertise.

In this tutorial we present FORMULA 2.0, which is formal framework for developing DSLs. FORMULA specifications are succinct descriptions of DSLs, and specifications can be immediately connected to state-of-the-art analysis engines without additional expertise. FORMULA provides: (1) succinct specifications of DSLs and compilers, (2) efficient compilation and execution of input programs, (3) program synthesis and compiler verification.

We take a unique approach to provide these features: Specifications are written as strongly-typed open-world logic programs. These specifications are highly declarative and easily express rich synthesis / verification problems. Automated reasoning is enabled by efficient symbolic execution of logic programs into quantifier-free constraints, which are dispatched to the state-of-the-art SMT solver Z3. FORMULA has been applied within Microsoft to develop DSLs for verifiable device drivers and protocols. It has been used by the automotive / embedded systems industries for software / hardware co-design under hard resource allocation constraints.

Tutorial Outline

This half-day tutorial introduces the FORMULA 2.0 language and tools through a series of small DSLs. We shall demonstrate DSLs that formalize: (1) a class of resource allocation problems subject to hard constraints, (2) a small functional programming language, and (3) a timed-automata style state machine language (with dense time). The first example illustrates DSLs that are not executable, but nonetheless have important synthesis problems (i.e. program synthesis amounts to solving resource allocation problems). The second example shows how to encode classic operational semantics using the power of fixed-point logic. The third example demonstrates more advanced concepts: dense time semantics, non-deterministic operational semantics, and symbolic model checking over background theories. The target audience is the practicing engineer interested in formalizing patterns and practices into actionable DSLs. While an understanding of logic and constraints is expected, no prior knowledge of FORMULA or logic programming is required. The examples are designed to introduce the necessary concepts.

Materials

A web interface to FORMULA 2.0 shall be made available, so no installation of software will be required. (The web interface for FORMULA 1.0 can be found at http://www.riseforfun.com/Formula. FORMULA 2.0 will also be integrated with RiseForFun.) This tutorial will be a condensed and more advanced tutorial based on the one to be presented at ICTAC 2013 in September (http://ictac2013.ecnu.edu.cn/). Consequently, a full 60 pages of curated lecture notes will be available for the HILT audience. For those users interested in installing a local copy of FORMULA 2.0, this option will also be available at no expense.

Monday Morning Tutorials (9:00am - 12:30pm)

MA1: Satisfiability Modulo Theories for High Integrity Development
Nikolaj Bjorner (Microsoft Research)

Audience and Prerequisites: Familiarity with basic concepts from programming languages and logic will be assumed. On the other hand the tutorial does not assume familiarity with how SMT solvers work or how to use them.

Satisfiability Modulo Theories (SMT) solvers are used in many modern program verification, analysis and testing tools. They owe their scale and efficiency thanks to advances in search algorithms underlying modern satisfiability solvers for propositional logic (SAT solvers) and first-order theorem provers, and they owe their versatility in software development applications thanks to specialized algorithms supporting theories, such as numbers and algebraic data-types, of relevance for software engineering.

This tutorial introduces SMT solvers in the context of development of high integrity software. We introduce the algorithmic principles of SMT solving, including the foundations of modern SAT solving search, integration with specialized theory solvers, and modules for quantifier reasoning. The second part of the tutorial shows how the capabilities of SMT solvers can be used in applications where a high degree of integrity is sought. To illustrate various uses of SMT solving we take as starting point some of the tools using the state-of-the-art SMT solver Z3 from Microsoft Research.

The introduction to the algorithms behind SMT solvers is aimed to give an idea of the capabilities of modern SMT solvers: what problems are a good fit for SMT solvers and what areas are challenging or out of scope. The applications examined in the second part of the tutorial include Pex (a tool based on symbolic execution), SecGuru (a tool used for firewall analysis), Dafny (a program verification environment), and FORMULA (a tool used for model based design). The tutorial use these examples to illustrate how SMT solvers are integrated within analysis tools and how to leverage the SMT solvers when using such tools.

Z3 is developed by Leonardo de Moura, Nikolaj Bjorner and Christoph Wintersteiger. There are online demos and tutorials available from http://rise4fun.com/z3py (a python based wrapper around Z3) and http://rise4fun.com/z3 (a text-based interface using the SMT-LIB2 language). Several tools shown on http://rise4fun.com use Z3 under the hood. Z3 binaries and the source code can be downloaded from http://z3.codeplex.com.

MA2: Practical Specification and Verification with CodeContracts
Francesco Logozzo (Microsoft Research)

Audience and Prerequisites: Some rough idea about what programming is.

In this tutorial I will introduce you to CodeContracts. CodeContracts are a language agnostic solution to the problem of specifying Contracts (preconditions, postconditions, and object invariants) that we have developed at Microsoft. They consists of a contract specification API (standard in .NET since v4.0) and a set of tools that consume contracts. Tools enable automatic documentation generation, compiler-independent runtime checking, and practical verification.

After recalling some basics on CodeContracts, I will describe cccheck, the CodeContracts static checker. Cccheck, unlike similar tools, is based on Abstract interpretation. This allows us to provide better performances, more automation by inferring loop invariants, and simple preconditions and postconditions

The CodeContracts tools are available online in the Visual Studio Gallery. They have been downloaded 100,000 times.

Monday Afternoon Tutorials (2:00 - 5:30pm)

MP1: Bounded Model Checking for High-Integrity Software
Sagar Chaki (Carnegie Mellon University Software Engineering Institute)

Audience and Prerequisites: Anyone looking for a hands on introduction to bounded model checking for software, e.g., someone with a background in software development, compilers, static analysis, software quality, programming languages etc. Preferred background:

Outline

  1. Overview of model checking (15 mins)
  2. Overview of SAT solving (15 mins)
  3. Bounded model checking of hardware - connecting model checking and SAT (20 mins)
  4. Bounded model checking of single-threaded C code (50 mins)
    1. Technical details (verification condition generation etc.)
    2. Live demonstration using the CBMC tool (http://www.cprover.org/cbmc)
  5. Bounded model checking of multi-threaded C code (30 mins)
    1. Technical details (sequentialization for multi-threaded code)
    2. Live demonstration using the CBMC tool
  6. Bounded model checking of periodic real-time software (50 mins)
    1. Technical details (sequentialization for periodic programs)
    2. Live demonstration using the REK tool (http://www.andrew.cmu.edu/user/arieg/Rek)
  7. Q&A (30 mins)

MP2: Service-Oriented Architecture (SOA) Concepts and Implementations
Ricky E. Sward (The MITRE Corporation), Jeff Boleng (Carnegie Mellon University Software Engineering Institute)

Audience and Prerequisites: This tutorial is targeted at the Beginner Level. No prerequisites or prior knowledge of SOA are required.

This tutorial explains how to implement a Service-Oriented Architecture (SOA) for reliable systems using an Enterprise Service Bus (ESB) and the Ada Web Server (AWS). The first part of the tutorial describes terms of Service-Oriented Architectures (SOA) including service, service registry, service provider, service consumer, Service Oriented Architecture Protocol (SOAP), and Web Service Description Language (WSDL). This tutorial also presents principles of SOA including loose coupling, encapsulation, composability of web services, and statelessness of web services. The tutorial also covers the benefits of SOA and organizations that are supporting SOA infrastructure. The second part of the tutorial covers the Enterprise Service Bus (ESB) including definitions, capabilities, benefits and drawbacks. The tutorial discusses the difference between SOA and an ESB, as well as some of the commercially available ESB solutions on the market. The Mule ESB is explored in more detail and several examples are given. In the third part, the tutorial covers the Ada Web Server (AWS) built using the Ada programming language. The tutorial covers the capabilities of AWS and explains how to build and install AWS. The tutorial explains how to build an AWS server and include the server in an Ada application. The tutorial demonstrates how to build a call back function in AWS and build a response to a SOAP message. Finally, the tutorial explains how to connect an AWS server to an ESB endpoint. AWS is a key component to building a SOA for a reliable system. This capability allows the developer to expose services in a high-integrity system using the Ada and SPARK programming languages.

Detailed Outline

  1. Introduction and Background
  2. Part 1 - Service-Oriented Architecture
    1. SOA Background Terminology: XML, XML Document, XSD, XSLT
    2. SOA Terminology: Service, Registry, Provider, Consumer, WSDL, SOAP, SLA
    3. SOA Message Patterns: Request/Response, Publish/Subscribe
    4. SOA Orchestration and Web Service Security
    5. Principles of SOA
    6. Benefits of SOA
    7. SOA Organizations: W3C, OASIS
  3. Part 2 - Enterprise Service Bus (ESB)
    1. ESB description and terminology
    2. Commercial ESB options
    3. ESB's and SOA
    4. Mule ESB Case Study and examples
      1. Mule endpoints
      2. Mule configuration file
  4. Part 3 - Ada Web Server (AWS)
    1. AWS definitions and capabilities
    2. Building and Installing AWS
    3. Building an AWS web server
    4. Building a call-back function
    5. AWS server example
    6. AWS and WSDLs
  5. Connecting AWS to Mule
    1. Configuration file
    2. Building an Ada web service
    3. Exposing an Ada web service
    4. Example
  6. Conclusions


Created on 29 May 2014;  website comments and corrections to ClydeRoby at ACM.Org