Miscellaneous

Miscellaneous Papers

Using OpenStack To Improve Student Experience in an H.E. Environment

by Stephen Bonner, Carl Pulley, Ibad Kureshi, Violeta Holmes, John Brennan and Yvonne James. Science and Information (SAI) Conference 2013

Abstract

The cloud computing paradigm promises to deliver hardware to the end user at a low cost with an easy to use interface via the internet. This paper outlines an effort at the University of Huddersfield to deploy a private Infrastructure as a Service cloud to enhance the student learning experience.

The paper covers the deployment methods and configurations for OpenStack along with the security provisions that were taken to deliver computer hardware. The rationale behind the provisions of virtual hardware and OS configurations have been defined in great detail supported by examples. This paper also covers how the resource has been used within the taught courses as a Virtual Laboratory, and in the research projects.

A second use case of the cloud for Automated Formative Assesment (AFA) by using JClouds and Chef for Continuous Integration is presented. The AFA deployment is an example of a Software as a Service offering that has been added on to the IaaS cloud. This development has led to an increase in freedom for the student.

Full paper: [PDF]

Advancing Research Infrastructure Using OpenStack

by Ibad Kureshi, Carl Pulley, John Brennan, Violeta Holmes, Stephen Bonner and Yvonne James. Journal of Advanced Computer Science and Applications

Abstract

Cloud computing, which evolved from grid computing, virtualisation and automation, has a potential to deliver a variety of services to the end user via the Internet. Using the Web to deliver Infrastructure, Software and Platform as a Service has benefits of reducing the cost of investment in internal resources of an organisation. It also provides greater flexibility and scalability in the utilisation of the resources. There are different cloud deployment models - public, private, community and hybrid clouds. This paper presents the results of research and development work in deploying a private cloud using OpenStack at the University of Huddersfield, UK, integrated into the University campus Grid QGG.

The aim of our research is to use private cloud to improve our High Performance Computing (HPC) research infrastructure and to provide flexible and scalable resources for research, teaching and assessment. As a result of our work we have deployed private QGG-cloud and devised a decision matrix and mechanisms required to expand HPC clusters into the cloud maximising the resource utilisation efficiency of the cloud.

As part of teaching and assessment of computing courses an Automated Formative Assessment (AFA) system was implemented in the QGG-Cloud. The system utilises the cloud's flexibility and scalability to assign and reconfigure required resources for different tasks in the AFA. Furthermore, the throughput characteristics of assessment workflows were investigated and analysed so that the requirements for cloud-based provisioning can be adequately made.

SSI Tools

Papers

Logical Methods in the Formal Verfication of Safety-Critical Software

by C.Pulley and G.V.Conroy. In the IMA Conference Proceedings: Mathematics of Dependable Systems, 1st - 3rd September 1993, Royal Holloway, University of London

Abstract

The purpose of the work reported in this paper is to describe a formal procedure by which one may automatically verify the safety of a specific SSI interlocking. Unlike other research work reported on elsewhere (see eg. [Mor93] and [IngMit92]), we shall explicitly model the IFPs polling cycle within the formalism to be presented shortly. This has the added benefit of enabling us to more correctly model the SSIs behavior and to also formally verify the safety of the IFP. Unlike [IngMit92], we are able to express and verify much more general safety properties. Our work also differs from the above in that we have concentrated on trying to improve the efficiency of our decision procedure rather than by concentrating on the modes by which we may verify certain types of safety property.

References:

  • [Mor93]: Morley, M., J. (1991) Modeling British Rail's Interlocking Logic: Geographic Data Correctness. LFCS Report ECS-LFCS-91-186, University of Edingburgh, November 1991.
  • [IngMit92]: Ingleby, M. and Mitchell, I. (1992) Proving Safety of a Railway Signaling System Incorporating Geographic Data. Proceedings SAFECOMP '92, 28th-30th October 1992, Zurich, Switzerland.

Full paper: [PDF]

Reports

Overview of the Proof Verifier

by C.Pulley. DTI/SERC "SSI Tools" Project, 1995, Nos.7.6

Abstract

This document defines (or rather shows how to!) a Floyd-Hoare programming logic for the SSI Data Language. This programming logic may easily (tediously?) be implemented using techniques from type checking.

Specification of the Proof Assistant

by C.Pulley. DTI/SERC "SSI Tools" Project, 1995, Nos.7.4

Abstract

This report provides a full specification in Z of the proof search algorithm.

The reachability algorithm specified in this report has been structured in a manner similar to the structuring of the various graph algorithms found in the works of Hopcroft and Tarjan. This has enabled a much more generic and flexible approach to the algorithms specification to be taken.

References:

  • Hopcroft, J.E. and Tarjan, R.E. (1973) Algorithm 447: Efficient Algorithms for Graph Maninpulation, Communications of the ACM 16(6), 372-378.
  • Tarjan, R.E. (1972) Depth-First Search and Linear Graph Algorithms, SIAM Journal of Computing 1(2), 146-160.

A Proof Calculus for the SSI Geographic Data Language

by C.Pulley. DTI/SERC "SSI Tools" Project, 1995, Nos.7.2

Efficient Inference Techniques for Verifying that an SSI is Safe/Unsafe

by C.Pulley. DTI/SERC "SSI Tools" Project, 1995, Nos.7.1

Description of the Concrete and Abstract Syntax for the SSI Geographic Data Language

by C.Pulley. DTI/SERC "SSI Tools" Project, 1994, Nos.6.1.2

Abstract

This document is essentially three separate documents all combined into one:

  • Firstly, we have an EBNF description of the concrete syntax for the SSI Data Language.
  • This EBNF description is presented alongside with a Z description of the abstract syntax of the SSI Data Language.
  • Finally, in appendix A, we have a prolog implementation of a parser for the SSI Data Language. The parser is written using the DCG grammar rules of prolog and the rules pass back a prolog implementation of the Z abstract syntax tree, having previously taken in a prolog implementation of the EBNF description of the concrete syntax tree.

Partial Semantics for the SSI Data Language

by C.Pulley. DTI/SERC "SSI Tools" Project, 1993, Nos.6.1.1

Abstract

This document, along with deliverables 6.1.2 and 6.1.3, provides a full syntactic and semantic specification (in the Z notation and a BNF like notation) of the SSI data language and the IFP.

Deliverable 6.1.3 provides a specification of the IFP and how it interacts with and uses information within the SSI data files.

This document describes a semantics for the various constructs used within the SSI data files to describe an interlockings functionality.

Semantics for the Interlocking Functional Program

by C.Pulley. DTI/SERC "SSI Tools" Project, 1993, Nos.6.1.3

Abstract

This document, along with deliverables 6.1.1 and 6.1.2, provides a full syntactic and semantic specification (in the Z notation and a BNF like notation) of the SSI data language and the IFP.

Deliverable 6.1.1 provides a specification of the SSI data language constructs that are used within the various SSI data files to specify an interlockings functionality.

This document describes how the IFP interacts with and uses the information within these SSI data files. The concepts of major and minor cycle are introduced to facilitate the description of the IFP.

Approaches for Automated Reasoning with Solid-State Interlockings and their Geographic Data

by C.Pulley. DTI/SERC "SSI Tools" Project, 1992, Nos.5.1

Abstract

This report introduces some logics that we suggest are of use in the formal specification of existing SSI geographic data. We then go on to show that validity for these logics is decidable.

For us this opens up the possibility of being able to automatically verify that properties hold of our SSI geographic data (in particular, we are here interested in the safety properties of a given railway layout).

The logics we propose to use are based on the second-order monadic theory of successor arithmetic.

Discussion Papers

Analysis of the use of Galois Theory to reduce Time/Space Complexities

by C.Pulley. DTI/SERC "SSI Tools" Project, 1994, Nos. U013

Abstract

The purpose of this technical note is to derive an intuitive representation for the clopen subsets of the topologies defined by Ingleby and Mitchell.

In doing this, we are able to show that the galois theory approach of Ingleby and Mitchell simply partitions the SSI data code up into control fragments that have no or little dependance upon each other. Unfortunately, the majority of railway layouts have lots of interactions and so their partitioning algorithm is of little help with the verification of such layouts.

References:

  • Ingleby, M. and Mitchell, I. (1992) Proving Safety of a Railway Signaling System Incorporating Geographic Data. Proceedings SAFECOMP '92, 28th-30th October 1992, Zurich, Switzerland.

PhD Papers

Papers

A Propositional Logic That Handles Conditional Probabilities

by C.Pulley. Unpublished

Abstract

In [FagHalMeg90], two logics for reasoning about probabilities were introduced. The first was unable to reason about conditional probabilities. To rectify this [FagHalMeg90] introduce their second probabilistic logic. However, unlike their first, they find it necessary to introduce quantifiers. In this paper we rectify this defect by presenting a propositional logic that can reason about conditional probabilities. Our method of proof is such that we may generalize it to encapsulate soundness and completeness for numerous other logics (eg. the first probabilistic logic of [FagHalMeg90]; fuzzy logic etc.). Our main requirement for these generalizations is that our logics should have a first-order metatheory.

References:

  • [FagHalMeg90]: Fagin, R., Halpern, J.Y., and Megiddo, N. (1990), A Logic for Reasoning about Probabilities, Information and Control Vol. 87 pp.78-128.

Full paper: [PDF]

MSc Papers

Papers

Pavelkan Logics on the unit Interval: Proof Boundaries and Sound and Complete Logics

by C.Pulley. Unpublished

Abstract

In [Pavelka], Pavelka gives a sound and complete axiomatisation for a logic that reasons with fuzzy sets of hypothesis and conclusions rather than just sets, as in (say) classical and intuitionistic logics.

This paper presents axiomatizations that are not only simpler than those presented in [Pavelka], but which also have simpler soundness and completeness arguments. In addition, we shall also be concerned with studying Pavelka's notions of soundness and completeness.

Pavelka determines soundness and completeness using a limit concept. More precisely, for any fuzzy set X and logical sentence θ:

∨ { a ∈ [0,1] | from X we may derive θ to degree a } = ∨ { a ∈ [0,1] | ∀ valuation W ≥ X · W(θ) ≥ a }
Since we are showing that limit values are equal in our P-soundness and P-completeness results, it should be no surprise that the associated deductive system may fail to derive the limit value, but still be able to derive all non-limit values (ie. those belief values strictly less than the limit value). This observation leads us to present a number of logics for which we may characterize the provable limit values.

In particular, we present a logic in which one may assume mutually inconsistent information, but one may not derive every sentence to every belief value!

References:

  • [Pavelka]: Pavelka, J. On Fuzzy Logic III: Semantical Completeness of some Many Valued Propositional Calculi Zeitshrift für Math. Logik und Grundlagen d. Math., Vol. 25, 1979.

Full Paper: [PDF]

Holly

Papers

Computer Arithmetic: Logic, Calculation and Rewriting

by M.Benini, D.Nowotka and C.Pulley. Frontiers of Combining Systems (FroCoS'98), October 2nd-4th 1998, University of Amsterdam

Abstract

This paper describes the concepts behind the Computer Arithmetic Toolkit (CAT) for the Isabelle/HOL system written by the authors.

Full paper: [PDF]

Workshop

Holly: An Approach to Object Code Verification

by M. Benini, S. Kalvala, D. Nowotka and C. Pulley. 5th Annual Automated Reasoning Workshop (ARW 5) Bridging the Gap between Theory and Practice co-located with the 14th BCTCS, St. Andrews, 1998.

Abstract

Formal verification of software typically consists in checking programs in a high-level language against an abstract specification. Confidence on the correctness of the actual program running on a machine also relies on the soundness of the translation from the high-level language to the machine code, i.e., the correctness of a compiler, including its code optimisation techniques.

If one wishes to have confidence on the final code, another approach is object code verification, i.e., verification of program code at assembly level. Now the confidence in the implementation of a program on an actual machine is more direct, relying on the correctness of the hardware model and no other software.

But, dealing with object code also has a price. It is, in a sense, further away from its specification because it has to deal with a more concrete machine, considering registers, limited memory, and so on. There is a vast shift in granularity between code and specification.

The technique for object code verification we are developing emphasises the use of abstraction, aided by a process algebraic framework. The concept of simulation provides the tool with which abstractions on the process algebraic representation of the program can be formalised.

However, the correctness proof takes place in higher-order logic (HOL), which we believe presents a more amenable proof environment. Abstraction at the logical level is obtained by unlifting results from the CCS level using the CCS semantics. More precisely, let < be a simulation relation, and let [| - |]^s be the lifting operator for a particular sequence s of states, then:

If P < Q then ∀ s · [| P |]^s ⇒ [| Q |]^s .
The interaction between the logical and the algebraic level is fundamental for our methodology.

We have implemented this approach in a proof system we call Holly. We use Isabelle/HOL, in which we embedded a variation of Milner's Calculus of Communicating Systems (CCS) as a process algebra. When verifying a program, its object code is translated both into a representation in HOL and an equivalent representation in CCS. At any point in a proof either deductions in HOL or simulations in the process algebra can be used.

Holly demonstrates the concurrent use of a logical and an algebraic model to make object code verification feasible. In this talk, we expand on the interaction between these models, and highlight the interaction within an example proof in Holly.

Code Releases

CAT is a Computer Arithmetic Toolkit for the Isabelle/HOL theorem prover. It provides a theory for integers, a rewrite engine for integer expressions, and a decision procedure for Presburger formulas.

Version 1.0 beta of CAT is available here which requires Isabelle94-8 and Poly ML 3.2.

  • Source code distribution: CAT.tgz
  • Documentation (also included in the distribution):