1,721,050 research outputs found
Modelling Control Process and Control Mode with Synchronising Orthogonal State Machines
No full textIn this short paper we describe early work on a case study concerning a power window control unit. We use UML-B state machines to simultaneously model both the cyclic processing schedule and the mode of control behaviour. We find this a useful way to visualise the model, particularly when the state machines are animated via the Pro-B animator. We verify the state machines using the Event-B proof tools. We envisage new developments to the UML-B tool set to improve support for this modelling technique. The motivation for this simple but powerful form of modelling is the immediate benefit and low cost of entry making industrial adoption of formal models more attractive to industry
UML-B: Formal modelling and design aided by UML
No full textThe emergence of the UML as a de-facto standard for object-oriented modelling has been mirrored by the success of the B method as a practically useful formal modelling technique. The two notations have much to offer each other. The UML provides an accessible visualisation of models facilitating communication of ideas but lacks formal precise semantics. B, on the other hand, has the precision to support animation and rigorous verification but requires significant effort in training to overcome the mathematical barrier that many practitioners perceive. We utilise a derivation of the B notation as an action and constraint language for the UML and define the semantics of UML entities via a translation into B. Through the UML-B profile we provide specialisations of UML entities to support model refinement. The result is a formally precise variant of UML that can be used for refinement based, object-oriented behavioural modelling. The design of UML-B has been guided by industrial applications
Exploring the barriers to formal specification
No full textThis thesis explores barriers to using formal specification for software development in industry. Empirical assessment techniques are used initially in an exploratory stage and subsequently in testing a hypothesis arising from the first stage. A second hypothesis is investigated by construction of a method and tool with subjective assessment of its effect. The first stage consists of a survey of experienced industrial formal methods users via a questionnaire-based interview. The interview explore the practicalities of using formal methods in an industrial setting. From the many findings in this stage, two hypotheses are selected for further investigation. The first hypothesis is that formal specification are no more difficult to understand than code. This is tested by formal experiment. The subject's ability to understand the functionality of a formal specification is compared with their ability to understand its implementation in program code. The second hypothesis is derived from observations, during the survey stage, that formal specifications are difficult to write. In particular, choosing appropriate abstractions is difficult. We consider what might make formal specification difficult and compare the process with that of programming. The second hypothesis is that a tool supported, graphical modelling notation would be of benefit in the process of writing a formal specification. Such a notation is devised by adapting the UML and augmenting it with a formal text notation. A tool that converts this graphical formal specification into the formal notation, B is described and examples of its use are analysed.</p
Using UML-B and U2B for formal refinement of digital components
No full textIn this paper we look at using formal methods to verify the transformation of a digital design from abstract functional specification to bit level implementation. As both authors are in-experienced in formal proof we saw this as a test of the practicality of introducing proof tools in an industrial setting rather than an exemplar of such methods Rigorous verification is desirable in digital design because mistakes can be extremely costly. However, there are drawbacks and barriers to introducing formal notations. Formal notations are abstraction hungry, viscous and require insight, experience and look-ahead. Hence we specialise the UML to alleviate these problems by providing a semi-graphical form of the formal notation B based on existing visual modelling tools. With a small case study, we show the use of B-UML using an event style of modelling to refine a macro level function into a cascade of single bit cells. We attempt to prove the refinement with the assistance of available proof tools but find that the problem is deceptively difficul
ERTMS Hybrid Level 3 - model using iUML-B/Event-B
No full textiUML-B based model of the ERTMS Hybrid Level 3 specification. Developed to support ABZ2018 case study track paper:
Diagram-led formal modelling using iUMLB for Hybrid ERTMS Level 3,
Dana Dghaym, Michael Poppleton, Colin Snook</span
iUML-B model of VLAN system
No full textDataset support the paper 'Analysing security protocols using refinement in iUML-B', presented at 9th NASA Formal Methods Symposium, 16-18 May 2017.
Formal specification of a VLAN tagging system illustrating the well-known security flaw of these systems, double-tagging. We use iUML-B class diagrams which provide a diagrammatic representation of the Event-B formalism. We specify the security principle that packets should only belong to nodes of a VLAN which they are intended for and prove that the property is maintained. We then refine the model to introduce the usual packet tagging mechanism that is supposed to ensure the security principle. A double tagging attack cannot be proven to satisfy the glueing invariant. A second version of the model is provided that excludes the Native LAN from being used as a VLAN which is the usual recommendation to prevent double-tagging attacks. This version is fully proven to be secure.</span
Rodin Prototype Plug-ins and Development of the SecBot Case Study
No full textDataset supporting "Refinement of Statecharts with Run-to-Completion Semantics"
Presented at FTSCS 2018 - The 6th International Workshop on Formal Techniques for Safety-Critical Systems, 16th November 2018, Gold Coast, Australia</span
- …
