1,721,164 research outputs found
Computability and complexity of unconventional computing devices
No full textWe discuss some claims that certain UCOMP devices can perform hypercomputation (compute Turing-uncomputable functions) or perform super-Turing computation (solve NP-complete problems in polynomial time). We discover that all these claims rely on the provision of one or more unphysical resources
Introduction
No full textThis chapter provides an introduction to the book Computational Matter, providing the historical background to the production of the book, and an overview of its scope and content
Retrenchment and the Mondex Electronic Purse (Extended Abstract)
No full textSome of the success stories of model based refinement are recalled, as well as some of the annoyances that arise when refinement is deployed in the engineering of large systems. The way that retrenchment attempts to alleviate such inconveniences is reviewed. The Mondex Electronic Purse formal development provides a highly credible testbed for examining how real world refinement difficulties can be treated via retrenchment. The contributions of retrenchment to integrating the real implementation with the formal development are surveyed, and the extraction of commonly occurring ‘retrenchment patterns’ is suggested
Retrenching the purse: The balance enquiry quandary, and generalised and (1, 1) forward refinements
No full textSome of the success stories of model based refinement are recalled, as well as some of the annoyances that arise when refinement is deployed in the engineering of large systems. The way that retrenchment attempts to alleviate such inconveniences is briefly reviewed. The Mondex Electronic Purse formal development provides a highly credible testbed for examining how real world refinement difficulties can be treated via retrenchment. The contributions of retrenchment to integrating the real implementation with the formal development are surveyed, and the extraction of commonly occurring ‘retrenchment patterns’ is recalled. One of the Mondex difficulties, the ‘Balance Enquiry Quandary’ is treated in detail, and the way that retrenchment is able to account for the system behaviour is explained. The problem is reconsidered using generalised forward refinement, and the simplicity of the resolution of the quandary, both by retrenchment, and by generalised forward refinement, inspires the creation of a genuine (1; 1) forward refinement for Mondex, something long thought impossible. The forward treatment exhibits a similar balance enquiry quandary to the backward refinement, as it must, given that both are refinements of an atomic action to a non-atomic protocol, and the forward quandary is dealt with as easily by retrenchment as is the backward case. The simplicity of the retrenchment treatment foreshadows a general purpose retrenchment Atomicity Pattern for dealing with atomic-versus-finegrained situations
Engineering and theoretical underpinnings of retrenchment
No full textRefinement is reviewed, highlighting in particular the distinction between its use as a specification constructor at a high level, and its use as an implementation mechanism at a low level. Some of its shortcomings as a specification constructor at high levels of abstraction are pointed out, and these are used to motivate the adoption of retrenchment for certain high level development steps. Basic properties of retrenchment are described, including a justification of the operation proof obligation, simple examples, its use in requirements engineering and model evolution, and simulation properties. The interaction of retrenchment with refinement notions of correctness is overviewed, as is a range of other technical issues. Two case study scenarios are presented. One is a simple digital redesign control theory problem, and the other is an overview of the application of retrenchment to the Mondex Purse development
Retrenching the Purse: Finite Exception Logs, and Validating the Small
No full textThe Mondex Electronic Purse is an outstanding example of industrial scale formal refinement, and was the first verification to achieve ITSEC level E6 certification. A formal abstract model and a formal concrete model were developed, and a formal refinement was hand-proved between them. Nevertheless, certain requirements issues were set beyond the scope of the formal development, or handled in an unnatural manner. The retrenchment Tower Pattern is used to address one such issue in detail: the finiteness of the purse log (which records unsuccessful transactions). A retrenchment is constructed from the lowest level model of the purse system to a model in which logs are finite, and is then lifted to create two refinement developments of the purse, working at different levels of detail, and connected via retrenchments, forming the tower. The tower development is appropriately validated, vindicating the design used
Retrenching the Purse: Hashing Injective CLEAR Codes, and Security Properties
No full textThe Mondex Electronic Purse is an outstanding example of industrial scale formal refinement, and was the first verification to achieve ITSEC level E6 certification. A formal abstract model and a formal concrete model were developed, and a formal refinement was hand-proved between them. Nevertheless, certain requirements issues were set beyond the scope of the formal development, or handled in an unnatural manner. The retrenchment Tower Pattern is used to address one such issue in detail: the use of a hash function rather than a total injective function when clearing the highly constrained purse logs. A retrenchment is constructed from the lowest level model to a model using a hash, and is then lifted to create two refinement developments, working at different levels of detail, and connected via retrenchments. The tower development is appropriately validated, vindicating the design used
Retrenching the Purse: Finite Sequence Numbers, and the Tower Pattern
No full textThe Mondex Electronic Purse system is an outstanding example of formal refinement techniques applied to a genuine industrial scale application, and notably, was the first verification to achieve ITSEC level E6 certification. A formal abstract model including security properties, and a formal concrete model of the system design were developed, and a formal refinement was hand-proved between them in Z. Despite this success, certain requirements issues were set beyond the scope of the formal development, or handled in an unnatural manner. Retrenchment is reviewed in a form suitable for integration with Z refinement, and is used to address one such issue in detail: the finiteness of the transaction sequence number in the purse funds transfer protocol. A retrenchment is constructed from the lowest level model of the purse system to a model in which sequence numbers are finite, using a suitable elaboration of the Z promotion technique. We overview the lifting of that retrenchment to the abstraction level of the higher models of the purse system. The concessions of the various retrenchments generated, formally capture the dissonance between the unbounded sequence number idealisation and the bounded reality. Reasoning about when the concession can become valid influences the actual choice of sequence number bound. The retrenchment-enhanced formal development is proposed as an example of a widely applicable methodological pattern for formal developments of this kind: the Tower Pattern
- …
