Adrian Hilton and Jon G. Hall.
Proving safety properties of fpgas.
Technical Report 2001/01, 2001.
[ bib |
FPGAs are increasing in complexity and being used as importantcomponents of safety-critical systems. Emergingsafety standards require analytic reasoning to demonstratethe safety of FPGAs in such systems. This report describesa method which uses a synchronous process algebra to produceformal proof that an FPGA program satisfies safetyproperties, and demonstrates its use in the specification ofsafety functions for a safety-critical system.
Pete Thomas and Carina Paine.
How students learn to program: Observations of practical work based
on tasks completed.
Technical Report 2001/02, 2001.
[ bib |
Lucia Rapanotti and Jon G Hall.
Educational java beans.
Technical Report 2001/03, 2001.
[ bib |
Educational Java Beans(tm) is a proposed extension to Enterprise Java Beans(tm). Its goals are: - to leverage the technology of Enterprise Java Beans to help the Educational Engineer;- to provide a uniform and scalable software platform upon which the development of distance learning and teaching system development can take place;- to provide suppoprt for the business processes of distance learning and teaching.In this paper we do four things. We describe relevant high-level business processes involved in distance learning and teaching, so to identify requirements for electronic support. We highlight the challenges of the current distance learning and teaching business model and explore meeting them through electronic support. We propose a new blueprint architecture - the EdJB architecture - that discharges these requirements and meets the challenges. Finally, we discuss the wider applicability of the new blueprint architecture in an enterprise setting.
Jon G. Hall and Tawanda Gurukumba.
Decomposing the dsub retrenchment.
Technical Report 2001/04, 2001.
[ bib |
The use of software has become prevalent in high integrity systems such as safety critical systems. The correctness of such software, i.e. thedelivery of a proper service that adheres to specified requirements, is a fundamental issue.Formal methods, which is a software development technique based on mathematics, addresses the issue of correctness of software. In theformal development of computer programs, a correctness- preserving transformation such as refinement may be used. Functional correctness is preserved by means of data refinement as well asalgorithmic refinement.One limitation of refinement is that it only works for operations of the same signature. In particular, in the concrete operation, some state variables may become input variables (e.g., when the variables denote values from some prior computations), some output variables may be added to the operations, and some variables may be constrained to a particular type (e.g., due to the finiteness of computer representation). In that case the signature of the concrete operation would be different from that of the abstract operation. The above techniques introduce the difference in signatures between abstract and concrete operations as a side effect but may be necessary in maintaining safe functionality in the concreteoperation.Retrenchment is a liberalized form of refinement that can be used to reason about functional correctness-preservation where operations may have different signatures. The Operation Retrenchment Proof Obligation is a predicate that characterizes the retrenchment of one operation by another. The proof obligation has slots for variouscharacteristics of a particular retrenchment, e.g., invariants, preconditions, operations, of the two machines involved in the retrenchment. Proving this proof obligation may provide structured proofs in terms of the proof steps required to discharge the operation retrenchment proof obligation. In particular, patterns in proofs can be coded into proof tactics enabling proofs to be automated.Automation enables the provision of software tools which may make the application of formal methods tractable, scalable and less prone to human error.
Carina Paine and Pete Thomas.
Observations of study time behaviour - comparisons of 1998 data &
Technical Report 2001/05, 2001.
[ bib |
AESOP (An Electronic Student Observatory Project) is a set of computer based data collection tools for recording, replaying and analysing student actions in LearningWorks, a Smalltalk programming environment. Students carrying out practical work using 'LearningBooks'. Each LearningBook contains a set of interrelated practical activities which the AESOP Recorder records together with a series of time and date stamps. A second tool, ‘The Analyser', analyses the recorded data. An initial trial of the system was undertaken in 1998.Since the initial trial the AESOP Recorder and Analyser have been refined for massive data collection. In 2000, data was collected from 200 students studying 22 of the course LearningBooks. This provided approximately 2000 recordings to analyse. The findings of these analyses are discussed here and are related to the conclusions reached after the first trial.
This file was generated by bibtex2html 1.98.