Software Technology Research Laboratory

Themes

DIF-DTC

UTC-SE

Technologies

Publications

Theses

Projects

NATO

FermaT	download flyer
AnaTempura	download flyer
SANTA	download flyer
Krit	download flyer
ITL Tools	ITL homepage
FermaT Maintenance Environment	download poster
Transformation Sequence Manager	download poster
Type System Editor	download poster
Clustering Techniques on Transformation Systems	download poster
Redocumentation for Legacy Systems	download poster
UML Diagram Extraction for Legacy Systems	download poster
De Montfort Creativity Assistant	download poster

FermaT: Program Transformation Toolkit

The FermaT Transformation System is a powerful industrial-strength program transformation system based on the WSL language.

The system uses formal proven program transformations, which preserve or refine the semantics of a program while changing its form. These transformations are applied to restructure and simplify the legacy systems and to extract higher-level representations.

By using an appropriate sequence of transformations, the extracted representation is guaranteed to be equivalent to the original code logic. The Wide Spectrum Language, called WSL is a logic-based formal method used for the transformation. Over many years a large catalogue of proven transformations has been developed, together with mechanically verifiable applicability conditions. These have been applied to many software development, reverse engineering and maintenance problems.

assembler listing

Theoretical Foundation

The theoretical work, on which FermaT is based, originated in research on the development of a language in which proofs of equivalence for program transformations could be achieved as easily as possible for a wide range of constructs. WSL is the "Wide Spectrum Language" used to support program transformation and includes low-level programming constructs and high-level abstract sp ecifications within a single language. This has the advantage that it is not necessary to differentiate between programming and specification languages: the entire transformational development of a program from abstract specification to detailed implementation can be carried out in a single language. During this process, different parts of the program may be expressed at different levels of abstraction. So a wide-spectrum language forms an ideal tool for developing methods for formal program development and also for formal reverse engineering.

A program transformation is an operation that modifies a program into a different form that has the same external behavior (i.e. it is equivalent under precisely defined denotation semantics). Since both programs and specifications are part of the same language, transformations can be used to demonstrate that a given program is a correct implementation of a given specification.

A refinement is an operation, which modifies a program to make its behavior more defined and/or more deterministic. Typically, the author of a specification will allow some latitude to the developer, by restricting the initial states for which the specification is defined, or by defining a nondeterministic behavior. For example, the program is specified to calculate a root of an equation, but is allowed to choose which of several roots it returns. In this case, a typical implementation will be a refinement of the specification rather than a strict equivalence. The opposite of refinement is abstraction: we say that a specification is an abstraction of a program, which implements it.

Example

An example of a transformation is reversing the branches in an if statement: if B then S1 else S2 fi is equivalent to: if not B then S2 else S1 fi

Applications

FermaT has applications in forward engineering (developing provably-correct software from high-level specifications), reverse engineering (determining the high-level specification of an existing software system) and language migration. FermaT has been used in several large-scale migration projects, transforming over a million lines of low-level assembler code into high-level structured and maintainable C. Examples are:

Tenovis offers modular communication solutions focusing on the convergence of telecommunications and the internet. At Tenovis, 200,000 clients throughout Europe are serviced by some 6,000 employees. In 2002, Tenovis generated revenue of about 950 million euros. One of Tenovis' products is a PBX system (Private Branch eXchange) running on four different hardware platforms and installed in sites spread across 18 countries. The system contains about 800,000 lines of C code, and 544,000 lines of 186 assembler: with the assembler split over 318 source files. FermaT was used to migrate all of the assembler code to high-level, structured, maintainable C code, suitable for porting to a more modern processor and also suitable for implementing a backlog of enhancements.
The Tesseract Corporation's main product is a Human Resources Management System (HRMS) which offers complete HR management capabilities, including payroll, HR administration, and benefits processing on the Web. The core of the system is implemented in IBM mainframe Assembler consists of 3,991 source files, copybooks and macros containing 691,000 lines of code which expands into 1.7Gb of listings when assembled. FermaT is being used to migrate this system to portable and maintainable C code capable of running efficiently on the mainframe and also on open systems platforms (including Linux PCs).

Licence

FermaT is available under the GNU GPL (General Public Licence) from the following web site:

http://www.tech.dmu.ac.uk/~mward/fermat.html

FermaT, together with an extended transformation catalogue, forms the core of the commercial FERMAT Migration and Comprehension Workbench produced by Software Migrations Ltd. (SML). The Workbench includes a number of tools for assembler analysis, comprehension and migration including dataflow analysers and program slicing.

FermaT program flowchart

Back

AnaTempura: Runtime Verification & Animation Toolkit

Assuring the correctness of hardware and software systems, like digital circuits and communications protocols, is a difficult task:

Complexity of the system.
Size of the system.
Requirements that need to be satisfied.

Several techniques have been proposed to assure the correctness of systems:

testing (simulators, debuggers, etc.),
formal methods, (theorem provers, proof checkers and model checkers),
runtime verification (simulators + theorem checkers).

Tempura is an executable subset of ITL. A formula is executable if

it is deterministic,
the length of the corresponding interval is known.
the values of the variables (of the formula) are known throughout the corresponding interval.

Tempura interpreter: takes a Tempura formula and constructs the corresponding sequence of states, i.e., interval. The C version of the Tempura interpreter was developed originally by Roger Hale in early 1985 by Roger Hale at Cambridge University. The first Tempura interpreter was programmed in Prolog by Ben Moszkowski, and was operational around December 2, 1983. Subsequently he rewrote the interpreter in Lisp (mid Mar, 1984), and in late 1984 modified the program to handle a two-level memory and multi-pass scanning.

AnaTempura, which is built upon the C version of Tempura, is a tool for the runtime verification of systems using Interval Temporal Logic (ITL) and its executable subset Tempura.

Runtime verification

Establish all desirable system properties (functional, timing, resource, . . . )
Insert at suitable places in the source code of the system assertion points
Use AnaTempura to check that the generated behaviour satisfies the desired properties

Assertion points: a sequence of changes, i.e., an interval (behaviour), will be generated when a program is running. For example the following factorial program with assertions

main()
{ long y, fac=1;
   assertion("fac", fac);
   text_out("Enter the seed:");
   scanf("%d",&y); assertion("y", y);
   while (y>1) {
     fac=fac*y; assertion("fac", fac);
     y=y-1; assertion("y", y);
   }
}

will generate the sequence:

!PROG: assert fac:1:!
!PROG: assert y:4:!
!PROG: assert fac:4:!
!PROG: assert y:3:!
!PROG: assert fac:12:!
!PROG: assert y:2:!
!PROG: assert fac:24:!
!PROG: assert y:1:!

The corresponding behaviour (interval):

fac behaviour

Location of assertion points is determined by the variables used in our property of interest. Simple search trough the source code will locate all places where the variables are changing. We will place the assertion points directly after those "places of change". This will ensure that behaviour generated during the runtime of the system is indeed the "correct" behaviour.

For the factorial example the property we want to check is:

define seed = 1 + (random mod 10).
define fac_rel(Y) = {
     if Y=seed then Y
     else Y* fac_rel(Y+1)
}.

The check:

define test() = {
     exists Fac,Y : {
       prog_send(seed);
       check(1,Fac,Y);
       if seed>1 then {
         while Y>1 do
          check(fac_rel(Y),Fac,Y)
       } else empty
    }
}.

Sample test run (seed is 10):

Tempura 1> run test().
!:: Pass Prog 10 Prop 10
!:: Pass Prog 90 Prop 90
!:: Pass Prog 720 Prop 720
!:: Pass Prog 5040 Prop 5040
!:: Pass Prog 30240 Prop 30240
!:: Pass Prog 151200 Prop 151200
!:: Pass Prog 604800 Prop 604800
!:: Pass Prog 1814400 Prop 1814400
!:: Pass Prog 3628800 Prop 3628800
Done! Computation length: 30.

Example of Program Animation

Letter sorter: a control program for sorting letters that uses 2 sensors and 2 solenoids.

A fragment of the C code is shown below.

scan_csensor (&class_sensor);
assertion("class", class_sensor);
if (class_sensor < 2) {
   SolOff(4); Delay(delay4,1);
   SolOn(4); Delay(delayF,4);
   scan_lsensor (&letter_sensor);
   assertion("lsens",letter_sensor);
   if ( !YellowSet ) {
     Delay(delay3A,2); SolOff(3);
     Delay(delay3B,3); YellowSet = 1;
   }
} else {
   SolOff(4); Delay(delay4,1);
   SolOn(4); Delay(delayF,4);
   scan_lsensor (&letter_sensor);
   assertion("lsens",letter_sensor);
   if ( YellowSet ) {
     Delay(delay3A,2); SolOn(3);
     Delay(delay3B,2); YellowSet = 0;
   }
}

Time is modelled as a variable:

! 0:: Solenoid 4 ON: Pass
! 10:: Class sensor 0: Pass
! 10:: Letter sensor 2: Pass
! 20:: Class sensor 1: Pass
! 20:: Solenoid 4 OFF: Pass
. . .

corresponds to following interval:

time behaviour

Screendump of the corresponding animation:

time behaviour

License

AnaTempura is available under the GNU GPL (General Public Licence) from the ITL homepage.

Back

SANTA:Security Analysis Toolkit for Agents

With the continuous expansion of the Internet and the growing amount of embedded software, accessing and operating in this open environment, new technologies are needed to address the arising complexity and its implication on the security of the system.

The agent approach is promising to solve some of the problems that arise in an open, decentralised environment. It allows the dynamic evolution of the system and reflects the autonomous organisations that contributing to the network. In this approach the system is composed of autonomous programs (agents), that aim to achieve specific goals.

Agents can communicate with other agents in the system, i.e. to request information, or specific services. Each agent is designed for a specific problem and therefore has a very specific set of skills. A group of cooperating agents is able to solve problems that are beyond the capabilities of each individual agent.

Security critical applications that are operating in an open environment, e.g. the Internet, are highly vulnerable to attacks. Most agents in the system are not benevolent, i.e. they have conflicting goals. Not all agents in the system will have the same level of trust.

Whilst some information is vital for trusted agents and must be available, other agents must not obtain this information. Examples are battle-field and business strategies, where information-leakage is critical and can lead to loss of life or property.

Beside mechanisms that ensure the confidentiality, integrity and non-repudiation of exchanged messages, it is necessary to be able to control and analyse the information flow in the system. Methodologies and tool-support that focus on the information-flow are needed. Furthermore security-policies in open systems are dynamic and must be able to change over time and on events. Security models that capture this requirement are needed.

Objective

To assist in the design of security-critical, distributed applications we are developing the SAnTA-Toolkit as an Integrated Development Environment (IDE) for secure agents in Data and Information Fusion. The workbench contains 3 major parts:

Formal Model

A formal model allows to proof properties of the system design. Mission critical and in military applications must be based on a sound formal model. In our formal model security and functional and temporal requirements are expressed in a uniform way. This uniformity allows the specification of dynamically changing security policies.

Design Language

Formal specifications are abstract. The implementation of a formal specification is an non-trivial task. To close the gap between the abstract specification and a concrete implementation, we provide the widespectrum language SAnTA-WSL. In this language both abstract specification and concrete implementation constructs are expressed. Sound refinement rules are applied to preserve the semantic from the specification to the implementation.

Tool-Support

Important for the success of every formal development approach is the provided tool-support. The range in which tool-support is needed is multifold:

Analysis Tools to assist analysts in the formal specification of requirements, i.e. that help in structuring requirements and that give intuition if the formal specification captures the informal requirement are extremely valuable, since they allow to detect inconsistencies early in the development process.
Design The refinement from the abstract specification toward the concrete design is difficult and needs to be supported by tools. For example tools can verify that design decisions do not violate the system specification or can suggest possible refinements to the system-designer.
Verification/Validation Tools that allow to automate proofs of properties on the abstract as well as the concrete level increase the trustworthiness of the developed system. Although the strength of formal methods is to preserve the semantics of the original specification, testing is still necessary to ensure that the implementation and machine level does not introduce errors. Tools that can automatically create test-suits from high-level specifications help in exhaustive testing.

Overview

This section describes the SAnTA-workbench in greater detail. The following diagram shows the different modules that constitute the SAnTA-workbench.

SANTA workbench

Formal Modelling

Our approach is aligned on the formal -to- applied axis. Based on a simple computational model with semantics given in Interval Temporal Logic (ITL), security and functional requirements are expressed at the same level of abstraction within a uniform formal framework.

SAnTA-Analyst Assists in writing highlevel specifications, supporting the analyst with structured views of informal system requirements and their formal specifications.
Tempura Allows to animate the high-level specification. This provides a feeling for the formal requirement description and helps to discover inconsistent and incomplete requirements.

SAnTA-WSL is a wide spectrum language, that overcomes the gap between abstract specification and implementation. Wide spectrum means that both abstract specification and concrete implementation is expressed in the same language. Sound refinement rules are used to stepwise refine the SAnTA-specification into implementable SAnTA-language constructs. During the refinement Design decisions are made. This does include choices in the Enforcement-Architecture, e.g. vigilant agents, that enforce their own security requirements or security enforcer models, that act as a firewall between the protected agent and its environment.

SAnTA-Designer Assists during the design-phase, by suggesting and validating design-decisions. The Designer manages common refinements patterns that represent architectural designs, i.e. security enforcement architectures. It also keeps track of the refinement-tra jectory.

The resulting program is translated into a concrete agent middle-ware, such as JADE or Cougaar, by the SAnTA-Compiler. This allows to utilise the research and development work that has been achieved in the recent years.

SAnTA-Compiler From the concrete SAnTA-WSL a translation takes place into a Java-based Agent middleware. This is automated by the SAnTA Compiler. An additional feature to insert assertion-points into the emitted source-code, that allows the runtime-validation of the executing system.

Analysis of the system design, and the validation of security properties on the designed system is important. With appropriate tool-support the formal development increases the trustworthiness of the system and allows to verify properties of the system.

PVS Our ITL-library for the PVS Specification and Verification System can be used to automate mathematical proofs of theorems about SAnTA WSL specifications.

Model checking is an extensive search over all possible behaviour of the system, w.r.t. a specific property. It can show that a property holds true for the system, or produces counter-examples, that indicate how the property can be violated.

LITE is a verifier for Interval Temporal Logic, which has been used for the automated verification of compositional correctness properties in small case studies.

The before-mentioned techniques do not scale well with the complexity of the specification. Another approach is to animate the specification. This allows the designer to detect inconsistencies and mismatches in the specification at a high level. This is important, because of the high development costs of formal methods.

SPAT

The Security Policy Analysis Tool (SPAT, see above picture) especially focus on the analysis of security policies. It allows to display access-control matrix, delegation matrix and information flow in a tabular representation. Queries can interactivly be made to limit the scope of the analysis to critical parts. Figure 1 shows the user interface of SPAT.

SPAT The Security Policy Analysis Tool (SPAT) extracts security properties from the system specification and displays them graphically as authorisation, delegation and obligation graphs. It uses Tempura to animate the graphs and is specially tailored to the analysis of access-control and permitted information-flow. Foolowing picture shows the graphical representation of permissable information flow for a security policy.

The red rectangles represent subjects (users) in the system. The green ovals represent objects that can be accessed by this users. The solid arrows show that the policy allows the direct information flow from a sub ject to an ob ject and vice versa. The dotted lines represent the transitive closure of the direct information flow. E.g. information can flow from Bob to Alice via the object Carolrecord. AnaTempura is an extension to the original Tempura interpreter, that allows the runtime-validation of executables. To achieve this, assertions are inserted in the executable, that are then validated against the formal specification.

Acknowlegement

This work is partially funded by the DIF-DTC through project 12.5.1, "Secure and Trusted Agents for Information Fusion".

Back

Krit: Nonlinear Aircraft Dynamics Analysis and Flight Clearance Toolkit

An investigation of aircraft dynamics at high angles of attack and intensive spatial manoeuvring is closely coupled with combat aircraft agility and also flight safety of all types of aircraft including passenger airliners.

The qualitative methods for nonlinear dynamical systems and bifurcation analysis are very efficient tools for investigation of nonlinear aircraft dynamics. These methods significantly complement the common engineering approach mostly based on linearization of motion equations and direct numerical simulation of aircraft dynamics.

Analysis of nonlinear aircraft dynamics

KRIT is Matlab Toolbox providing numerical realization of methods from the nonlinear dynamic system theory and bifurcation analysis. KRIT is an excellent computational environment for solving nonlinear flight dynamics problems (inertia rollcoupling, wing rock, high incidence departures, spin). In engineering applications KRIT bridges the gap between classical linear analytical methods and real requirements for flight clearance of new aircraft (see above picture).

Mathematical Background

An aircraft dynamics can be described by an autonomous nonlinear dynamical system depending on a number of parameters such as control inputs, aircraft parameters, flight conditions, etc. (see following picture):

mathematical model

The basic KRIT algorithms allow user compute all possible equilibria, steady periodical orbits, complicated steady attractors at some fixed values of parameters (see next picture).

critical solutions of nonlinear system

The efficient continuation algorithm supports computation of attractor characteristics at variation of the system parameters. For every stable attractor KRIT can perform the computation of a region of attraction.

The computational algorithms in the current version of KRIT provide a high level of automation. The KRIT front end GUI's allow user to perform rather complicated investigation of aircraft critical flight regimes in support of flight clearance purposes. The GUI's for continuation analysis, manoeuvre design and flight clearance are presented in next two pictures, respectively.

Continuation database gui

Example of computation of flight envelop in the plane of angles of attack and sideslip is presented in the next picture.

computation of manoeuvre flight envelope