Structuring real-time Object-Z specifications

This paper presents a means of structuring specifications in real-time Object-Z: an integration of Object-Z with the timed refinement calculus. Incremental modification of classes using inheritance and composition of classes to form multi-component systems are examined. Two approaches to the latter are considered: using Object-Z's notion of object instantiation and introducing a parallel composition operator similar to those found in process algebras. The parallel composition operator approach is both more concise and allows more general modelling of concurrency. Its incorporation into the existing semantics of real-time Object-Z is presented.

Refining specifications to logic programs

The refinement calculus provides a framework for the stepwise development of imperative programs from specifications. In this paper we study a refinement calculus for deriving logic programs. Dealing with logic programs rather than imperative programs has the dual advantages that, due to the expressive power of logic programs, the final program is closer to the original specification, and each refinement step can achieve more. Together these reduce the overall number of derivation steps. We present a logic programming language extended with specification constructs (including general predicates, assertions, and types and invariants) to form a wide-spectrum language. General predicates allow non-executable properties to be included in specifications. Assertions, types and invariants make assumptions about the intended inputs of a procedure explicit, and can be used during refinement to optimize the constructed logic program. We provide a semantics for the extended logic programming language and derive a set of refinement laws. Finally we apply these to an example derivation.

Developing logic programs from specifications using stepwise refinement

In this paper we demonstrate a refinement calculus for logic programs, which is a framework for developing logic programs from specifications. The paper is written in a tutorial-style, using a running example to illustrate how the refinement calculus is used to develop logic programs. The paper also presents an overview of some of the advanced features of the calculus, including the introduction of higher-order procedures and the refinement of abstract data types.

Proving Temporal Properties of Z Specifications Using Abstraction

This paper presents a systematic approach to proving temporal properties of arbitrary Z specifications. The approach involves (i) transforming the Z specification to an abstract temporal structure (or state transition system), (ii) applying a model checker to the temporal structure, (iii) determining whether the temporal structure is too abstract based on the model checking result and (iv) refining the temporal structure where necessary. The approach is based on existing work from the model checking literature, adapting it to Z.

Prototyping Behavioural Specifications in the.NET framework

Over the last decade, software architecture emerged as a critical design step in Software Engineering. This encompassed a shift from traditional programming towards the deployment and assembly of independent components. The specification of the overall system structure, on the one hand, and of the interactions patterns between its components, on the other, became a major concern for the working developer. Although a number of formalisms to express behaviour and supply the indispensable calculational power to reason about designs, are available, the task of deriving architectural designs on top of popular component platforms has remained largely informal. This paper introduces a systematic approach to derive, from behavioural specifications written in Ccs, the corresponding architectural skeletons in the Microsoft .Net framework in the form of executable C] code. Such prototyping process is automated by means of a specific tool developed in Haskell

Design Guide and Construction Specifications for National Pollutant Discharge Elimination System (NPDES) Site Runoff Control, 2006

According to the 1972 Clean Water Act, the Environmental Protection Agency (EPA) established a set of regulations for the National Pollutant Discharge Elimination System (NPDES). The purpose of these regulations is to reduce pollution of the nation’s waterways. In addition to other pollutants, the NPDES regulates stormwater discharges associated with industrial activities, municipal storm sewer systems, and construction sites. Phase II of the NPDES stormwater regulations, which went into effect in Iowa in 2003, applies to construction activities that disturb more than one acre of ground. The regulations also require certain communities with Municipal Separate Storm Sewer Systems (MS4) to perform education, inspection, and regulation activities to reduce stormwater pollution within their communities. Iowa does not currently have a resource to provide guidance on the stormwater regulations to contractors, designers, engineers, and municipal staff. The Statewide Urban Design and Specifications (SUDAS) manuals are widely accepted as the statewide standard for public improvements. The SUDAS Design manual currently contains a brief chapter (Chapter 7) on erosion and sediment control; however, it is outdated, and Phase II of the NPDES stormwater regulations is not discussed. In response to the need for guidance, this chapter was completely rewritten. It now escribes the need for erosion and sediment control and explains the NPDES stormwater regulations. It provides information for the development and completion of Stormwater Pollution Prevention Plans (SWPPPs) that comply with the stormwater regulations, as well as the proper design and implementation of 28 different erosion and sediment control practices. In addition to the design chapter, this project also updated a section in the SUDAS Specifications manual (Section 9040), which describes the proper materials and methods of construction for the erosion and sediment control practices.

Review of Inconsistencies Between SUDAS and Iowa DOT Specifications, May 2006

The objectives of this multi-part project were to review the Iowa DOT Specifications and SUDAS Specifications section by section and develop recommendations for possible changes that will allow the two specifications to be used together.

Standards and specifications to manage accessibility issues in e-learning

Standards and specifícations to manage accessibility issues in e-learning