The problem

Currently, computers cannot be relied upon to resolve ambiguities that are naturally present in human-generated engineering specifications. Sometimes, those ambiguities are an inevitable consequence of the medium used (e.g. the English language, block diagrams), but sometimes they could be avoided if a more standardised approaches to design and requirement engineering were adopted. This exploratory work illuminates the most common sources of ambiguity and provides partial solutions and tools for coping with it.

The project has two distinct strands: formalisation of hybrid system designs and formalisation of engineering requirements. As a starting point for the former, we chose Simulink diagrams; more specifically, the A350 autobrake model was used throughout as a case-study and a driving example. On the side of the requirements, we began with the original set of functional requirements for the braking system. The two strands then converged in their common formal basis, for which we chose the mathematical theory of hybrid satisfiability and the formal verification tool HySAT.

The approach

The first major topic of this work was formalisation of Simulink diagrams as HySAT models. More specifically, it was necessary to embed the models in a suitable state space (the DECL section of a HySAT input file), determine the initial state(s) of the model (the INIT section) and the relationships between present and future states (TRANS). We used the A350 autobrake design as the driving example for this task.

We elected to assign a variable to every signal in a Simulink model. The types and ranges of these variables were obtained by manually setting them for the input variables and then automatically propagating them through the model. This kind of inference was automatically performed for the entire diagram, resulting in setting the types and ranges of 81% of signals. The remaining 19% were involved in feedbacks, where the described method fails, and they were treated as reals with wide ranges. This data was then appropriately formatted as a DECL section of a HySAT input file.

We have prepared an association table linking the textual and the formal descriptions of basic system properties (for example, “the autobrake is disarmed" would be linked to a formula such as “AB ARMED = false"). This was then used to automatically translate the structured requirement to a HySAT formula, where the connectives and their nesting would be determined by the structure of the requirement, and their arguments (operands) would correspond to the formal descriptions of basic properties. The resulting formulae formed the TARGET section of a HySAT input file.

We translated several requirements in this way and ran HySAT to verify them. In most cases the requirements were satisfied; when they were not, insights into the model and the requirements themselves were the result.

"The internship at Airbus UK gave me the opportunity to meet some of the finest industrial R&D minds. Perhaps the most valuable experience I gained from interacting with them is the appreciation of the differences in industrial and academic approaches to research and the realisation that the purest route is not always the shortest one. Last but not least, the internship provided a welcome distraction from my day-to-day research tasks. I would certainly recommend considering a PhD internship to any curious and open-minded research student," said intern, Marek Kwiatkowski.