Search

Computing is a rigorous, intellectually rich discipline alongside Maths, Science, or History. Like those subjects, Computing explores foundational principles and ideas, rather than training students in skills that date quickly. In an increasingly digital, knowledge-based age, Computing is fundamental both to full citizenship, and to our economic health as a nation. Yet, incredibly, Computing is virtually absent from UK schools. Instead, secondary schools in England currently teach ICT. The original concept behind ICT was to teach students how to use software to solve real-world problems. That would have been a tremendous achievement had it succeeded. However, what has actually happened in far too many schools is that ICT focuses solely upon IT literacy, and supporting teaching and learning in other curriculum contexts. ICT is not the discipline of understanding and knowledge of computers and the way they work.The creation of the EBac provides the perfect opportunity to send a clear signal to schools and pupils of the importance of Computing. Our key recommendation is that Computing (unlike ICT) should “count” towards the English Baccalaureate.On behalf of Computing at School:Dr. John WoollardProf. Simon Peyton-JonesDr. Bill Mitchell

The IRMOS project is developing tools and techniques for modelling, simulating, analysing, and planning real-time applications on service oriented infrastructures. These tools and techniques support the processes involved in designing, developing, deploying and executing applications where guaranteed QoS is needed. The report considers the value-chain for real-time applications hosted by third-party service providers. In the context of this value chain, we analyse who might benefit from the use of models, how and why these models might be used, and when during the application lifecycle modelling is most useful. Techniques are presented for building models of real-time applications including the use of stochastic process algebras, finite state automata, workflow models (e.g. BPEL, BPMN and YAWL) and specification languages (e.g. UML MARTE). The report discusses how these models need to be supported by estimation of application resource consumption, e.g. through benchmarking and fitting, and how mapping techniques allow models to be built for different actors in the value chain, e.g. for application providers and infrastructure providers. Tool support is also discussed e.g. PRISM for probabilistic model checking and Visual Service Composition Studio for service-oriented modelling. A detailed and specific real-time application scenario is included and modelled to allow the various techniques presented in this document to be demonstrated and quantitatively evaluated. The scenario also reveals the level of detail needed in order for meaningful modelling to be achieved in practice. The modelling scenario has been carefully engineered to be as representative as possible of the broad range of application characteristics encountered in the three reference IRMOS applications (film postproduction, eLearning, virtual and augmented reality). The modelling techniques discussed and then demonstrated in this report include identifying what resources are necessary to support an application, when those resources will be required during the application workflow, what performance is needed from them (i.e. QoS) and what will happen to the application if the required performance is not delivered. All of these are essential when developing and then agreeing service level agreements between the various entities in a service oriented infrastructure.

Presentation at a satellite workshop to 7th International Conference on integrated Formal Methods. Presentation discussed synthesis of real-time performance models for black box processes. The behavioural models were defined as timed stochastic finite state machines. An implementation of these models in PRISM was demonstrated.

Scenario based requirements specifications are the industry norm for defining communicating systems. These scenarios are often captured in the form of UML/MSC sequence diagrams. Errors are often introduced at this stage of the development process, which are costly to resolve if they are not detected early. This paper is concerned with the automatic detection and resolution of semantic errors that can occur in such scenarios.The paper discusses a semantic interpretation of scenario-based requirements and various types of defects (or pathologies) that can be detected. The paper defines the semantics and defects within a partial order theoretic framework. We introduce a UML 2.0 profile that captures various domain specific communication semantics, which can be used to determine the relevance of detected pathologies when different underlying implementation assumptions are made. The paper also discusses how to automatically resolve pathologies by using this profile to adapt the communication architecture in the requirements model.

Requirements for systems involving communicating processes (e.g. telecommunication systems) are often described with the aid of graphical notations, such as: Unified Modelling Language (UML), Message Sequence Charts (MSC) or Specification and Description Language (SDL). In using these notations to define requirements engineers tend to think of the most obvious behaviours of the system first (e.g. common system scenarios). However, depending upon the semantics of the graphical notation, specifications may also include non-obvious behaviours that at first glance are not apparent to the engineer when developing the specification. The method described here categorises tests that are automatically generated from a specification according to some suitable numerical weight. The idea is to define a weighting scheme that differentiates the most obvious behaviours from the non-obvious behaviours. In doing so, the user can quickly assess which test scripts represent the obvious behaviours, and consequently can concentrate on making sure that the most obvious behaviours are covered first.

Around a third of significant faults in embedded systems are caused by defective requirements specifications. Industrial case studies using existing techniques to construct analytical requirements models have been frustrated because of imprecise compositional semantics in the industrial specifications. The paper describes a method for synthesising analytical models from imprecise MSC requirements specifications that ensures the models reflect the intended compositions, and not those that result from the imprecision within the requirements.

This invention describes how to translate phase transition requirements defined with a graphical notation such as MSC-s or UML sequence diagrams into a form of abstract implementation which is useful for analysing feature combinations. This leads to a methodology for detecting feature conflicts in a partially specified system.

The paper defines a formal semantics for MSC scenarios that is a weakening of the state semantics from [6], whilst permitting some additional semantics in the spirit of Live Sequence Charts (LSCs) [4]. The semantics here differs from that of LSCs in that mandatory behaviour is defined dynamically within the domain of possible scenarios. This permits a semantics which uses domain knowledge to define when compositions of imprecise requirements are valid. This has been implemented by Motorola UK Research Labs, and is being used in a pilot study for a new telecommunications mobile 3G handset.

Specifications for wireless telecommunications systems are often only partially defined. It is also common for the specification to consist of a set of normative scenarios together with scenarios for some of the more important exceptional behaviours. A major challenge is to find effective means of detecting feature interaction conflicts contained in such specifications. Moreover the detected conflicts should be of value in debugging the specifications and should not be cluttered with inconsequential errors that are due to the incompleteness of the specifications. The paper describes a technique for constructing a phase automaton that can be used to statically analyse the specification scenarios in order to detect certain types of interactions between them, known as phase transition conflicts. There is anecdotal evidence to suggest that these kinds of inconsistency can account for a significant proportion of feature interactions. The phase automaton is intended primarily for the purpose of detecting these phase transition errors. This means the state space in the automaton only need include that part of the feature behaviour that is significant for those conflicts. This results in a small automaton that tends to make the conflict detection problem tractable.

Current approaches for generating tests for telecommunication systems produce scripts that execute a single sequence of actions that verify the implementation under test (IUT) has performed correctly. However, in recent years testing languages, such as TTCN, have been enhanced to facilitate the notion of concurrent testing. Where, a concurrent test script consists of a number of concurrent test components that interact to perform a particular test. This invention describes how to produce the co-ordination messages that are necessary to synchronise concurrent test components in order to check that an IUT exhibits the correct order of events. Note that we assume coordinating messages have a suitably small latency (delay), and the specification does not contain any race conditions.

Each Girard quantale (i.e. commutative quantale with a selected dualizing element) provides a support for a semantics for linear propositional formulas (but not for linear derivations). Several constructions of Girard quantales are known. We give two more constructions, one using an arbitrary partially ordered monoid and one using a partially ordered group (both commutative). In both cases the semantics can be controlled be a relation between pairs of elements of the support and formulas. This gives us a neat way of handling duality.

MSC-s specifying system requirements can be used to generate test scripts in languages such as TTCN. In 1996 TTCN was extended in order to describe concurrent test scripts. We give a characterisation of which concurrent tests can be executed by parallel test components (PTC-s) acting in concert. We also characterise when the PTC-s give the correct test result verdict.

This paper shows that many simulation equivalences over processes can be characterised by a single parameterised modal logic formula. Strong bisimulation equivalence was shown by Milner to be characterised in this way. This paper shows that simulation, complete simulation, ready simulation, 2-nested simulation, weak bisimulation and congruence can also be characterised in this way. The paper constructs a template which can be used to generate a parametrised modal formula which is guaranteed to characterise a 'sensible' simulation equivalence. Two infinite families of simulation equivalences are characterised in this way, both of which converge to strong bisimulation. The paper defines a similar template for weak simulation equivalences. This template is used to construct an infinite family of equivalences which converges to weak bisimulation equivalence, and another infinite family which converges to congruence.