Towards a Body of Knowledge in Formal Methods for the Railway Domain: Identification of Settled Knowledge

Bodies of Knowledge (BoK) are available only in mature technical fields, in which professional practices and technical rules have been well established (i.e.: ‘settled’), and are compiled for any prospective or current practitioner to refer to. By their factual establishment they also become professionally normative to a considerable extent. As a precursor to establishing a BoK it is important to determine whether or not a target domain already contains sufficient ‘settled’ knowledge, and, if yes, how such knowledge can be identified for its reproduction. In the undisputed safety-critical railway domain, formal methods have been applied for several decades in the solution of various modelling and verification problems. The application of many of those formal methods in the railway domain has also reached sufficient levels of maturity or ‘stability’ — yet no BoK for this domain has ever been compiled so far. Thus the time is ripe now to start such a project. In this paper, with regard to the necessary identification of settled knowledge, we apply the lattice-theoretical methods of Formal Concept Analysis (FCA) in order to structure and organise large amounts of relevant bibliometric data from the railway domain’s corpus of literature. In other words, we construct a formal concept lattice, the semantics of which is suitable for revealing the ‘settled’ parts of this domain. As a result of our formalised domain analysis, we provide a clear and theoretically well-grounded indication of the ‘settled’ themes and topics which any future BoK on Formal Methods in the Railway Domain ought to contain.