1,721,617 research outputs found
Letters from May and June 1950 from Gerald Butler Michael O\u27Connor to Zilla Linford Richards
No full textTwo letters, dated 16 May 1950 and 29 June 1950 from Gerald Butler Michael O\u27Connor at Barnards Mead, Devonshire, England, to Zilla Linford Richards before her planned visi
PVS Embedding of cCSP Semantic Models and their Relationship
No full textAbstractThis paper demonstrates an embedding of the semantic models of the cCSP process algebra in the general purpose theorem prover PVS. cCSP is a language designed to model long-running business transactions with constructs for orchestration of compensations. The cCSP process algebra terms are defined in PVS by using mutually recursive datatype. The trace and the operational semantics of the algebra are embedded in PVS. We show how these semantic embeddings are used to define and prove a relationship between the semantic models by using the powerful induction mechanism of PVS
On Proving with Event-B that a Pipelined Processor Model Implements its ISA Specification
No full textMicroprocessor pipelining is a well-established technique that improves performance and reduces power consumption by overlapping instruction execution. Verifying, however, that an implementation meets this ISA specification is complex and time-consuming. One of the key verification issues that must be addressed is that of overlapping instruction execution. This can introduce hazards where, for instance, a new instruction reads the value from a register which will be written by an earlier instruction that has not yet completed. Using Event-B’s support for refinement with automated proof, a method is explored where the abstract machine represents directly an instruction from the ISA that specifies the effect that the instruction has on the microprocessor register file. Refinement is then used systematically to derive a concrete, pipelined execution of that instruction. Microarchitectural considerations are raised to the specification level and design choices can be verified much earlier in the flow. The method proposed therefore has the potential to be integrated into an existing high-level synthesis methodology, providing an automated design and verification flow from high-level specification to hardware
Supporting reuse mechanisms for developments in event-b: composition
No full textThe development of specifications often is a combination of smaller sub-components. Focusing on reuse, an interesting perspective is to formally define the combination of sub-components through refinement steps, reusing their properties and generating larger systems. The previous situation suggests the application of a reuse mechanism: composition. Event-B is a formal method that allows modelling and refinement of systems. The combination and reuse of existing sub-components is not currently supported in Event-B. We propose the development of composition by extending the Event-B formalism as an option for developing larger models, focusing in distributed systems. A tool is developed to support the shared event composition in the Rodin platform. Properties and proof obligations of sub-components are reused and sufficient proof obligations are generated to ensure valid composed models
FM 2011: Formal Methods - 17th International Symposium on Formal Methods, Limerick, Ireland, June 20-24, 2011
No full text- …
