1,460 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
Refining Nodes and Edges of State Machines
No full textState machines are hierarchical automata that are widely used to structure complex behavioural specifications. We develop two notions of refinement of state machines, node refinement and edge refinement. We compare the two notions by means of examples and argue that, by adopting simple conventions, they can be combined into one method of refinement. In the combined method, node refinement can be used to develop architectural aspects of a model and edge refinement to develop algorithmic aspects. The two notions of refinement are grounded in previous work. Event-B is used as the foundation for our refinement theory and UML-B state machine refinement influences the style of node refinement. Hence we propose a method with direct proof of state machine refinement avoiding the detour via Event-B that is needed by UML-B
Comprehensibility of UML-B - A Series of Controlled Experiments
No full textThis paper summarises two controlled experiments conducted on a model that integrates the use of semi-formal notation, the Unified Modelling Language (UML) and a formal notation, B. The experiments assessed the comprehensibility of the model, namely UML-B. The first experiment compared the comprehensibility of a UML-B model and a B model. In the second experiment, the model was compared with an Event-B model, a new generation of B. The experiments assessed the ability of the model to present information and to promote problem domain understanding. The measurement focused on the efficiency in performing the comprehension tasks. The experiments employed a cross-over design and were conducted on third-year and masters students. The results suggest that the integration of semi-formal and formal notations expedites the subjects’ comprehension tasks with accuracy even with limited hours of training
Comprehensibility of UML-based Formal Model – A Series of Controlled Experiments
No full textThis paper summarises two controlled experiments conducted on a model that integrates the use of semi-formal notation, the Unified Modelling Language (UML) and a formal notation, B. The experiments assessed the comprehensibility of the model, namely UML-B. The first experiment compared the comprehensibility of a UML-B model and a B model. In the second experiment, the model was compared with an Event-B model, a new generation of B. The experiments assessed the ability of the model to present information and to promote problem domain understanding. The measurement focused on the efficiency in performing the comprehension tasks. The experiments employed a cross-over design and were conducted on third-year and masters students. The results suggest that the integration of semi-formal and formal notations expedites the subjects’ comprehension tasks with accuracy even with limited hours of training
Dataset for: Domain-Specific Scenarios for Refinement-based Methods
No full textAbstract Scenarios and related models for the HL3 case study described in: Snook, C., Hoang, T. S., Dghaym, D., Salehi Fathabadi, A., & Butler, M. (2020). Domain-Specific Scenarios for Refinement-based Methods. Journal of Systems Architecture. </span
Towards a method for rigorous development of generic requirements patterns
No full textWe present work in progress on a method for the engineering, validation and verification of generic requirements using domain engineering and formal methods. The need to develop a generic requirement set for subsequent system instantiation is complicated by the addition of the high levels of verification demanded by safety-critical domains such as avionics. Our chosen application domain is the failure detection and management function for engine control systems: here generic requirements drive a software product line of target systems. A pilot formal specification and design exercise is undertaken on a small (twosensor) system element. This exercise has a number of aims: to support the domain analysis, to gain a view of appropriate design abstractions, for a B novice to gain experience in the B method and tools, and to evaluate the usability and utility of that method.We also present a prototype method for the production and verification of a generic requirement set in our UML-based formal notation, UML-B, and tooling developed in support. The formal verification both of the structural generic requirement set, and of a particular application, is achieved via translation to the formal specification language, B, using our U2B and ProB tools
Parental contribution and spawning performance in captive common snook Centropomus undecimalis broodstock
No full textCommon snook are a species relatively new to aquaculture and to date, virtually no information is available on captive broodstock spawning characteristics. Understanding basic and fundamental data such as broodstock contribution of captive mass spawning snook is important, not only for the development of a successful selective breeding program for the species, but also for restocking wild fisheries and maintenance of local genetic variation. A scoping study was undertaken to explore the potential of DNA profiling for monitoring mating outcomes in captive snook. Spawning success was monitored among wild harvested broodstock that were undergoing hormonal treatment to induce spawning. The broodstock were maintained in three separate tanks (Tank A: 18 males and 15 females; Tank B: 22 males and 11 females; Tank C: 40 males and 16 females) and were subject to different handling stresses. Sixteen mass spawning events were studied across the three tanks over a 15month period. DNA profiling of eight microsatellite markers was employed to detect and quantify individual parental contributions for 2,154 larvae obtained from the three tanks. The panel of loci was generally robust and allowed unambiguous assignment of 89% of larvae to a single family. All spawns occurred within approximately 24 to 72hours post-implantation and only females implanted with gonadotropin releasing hormone analogue (GnRHa) were found to contribute. Overall, spawning performance among the three tanks was highly variable in terms of the total number of eggs produced (from 86,300 to 2,378,000 per spawn), fertilization success (from 17.0 to 87.3%) and hatch rate (from 47.8 to 98.1%). Three-day larval survival ranged from approximately 25.9 to 90.1% in tank A and 19.9 to 74.2% in tank C. During this study, new information regarding requirements for broodstock husbandry, mating patterns and spawning periodicity of captive common snook broodstock were obtained. Spawn contribution data 1) provided a confirmation of GnRHa treatment efficacy in female snook with a minimum stage of oogenesis (late secondary growth-SGl) required for successful spawning; 2) identified a potential impact of handling on maturation and spawning in male and female broodstock; 3) confirmed that, through photothermal conditioning, captive common snook broodstock can spawn over consecutive days and several times per year, including outside of their natural spawning season
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
- …
