Checking audit trails for measuring instruments using runtime verification

1. Introduction

Measuring instruments used in legal metrology are increasingly controlled by software, and the software embedded in those instruments has become a critical factor affecting the reliability of measurements. The international document OIML D 31 [1] specifies general software requirements and serves as guidance for the development of instrument-specific software requirements. When preparing international recommendations for particular types of measuring instruments, such as non-automatic weighing instruments and fuel dispensers, relevant requirements of OIML D 31 may be adopted and tailored to the needs of those instruments.

OIML D 31 identifies the prevention of interventions and the availability of evidence of such interventions as important concepts for measuring instruments. That is, interventions such as software updates and parameter changes shall be managed in such a way that their occurrence can be verified afterward.

In particular, when users are allowed to adjust legally relevant parameters, measuring instruments are required to provide a facility that automatically records any such adjustments in a non-erasable manner. One means explicitly described in OIML D 31 for fulfilling this requirement is an audit trail. An audit trail is a log that records events occurring within a measuring instrument together with their timestamps, thereby providing evidence of interventions. By examining the audit trail, it is possible to identify what interventions have occurred and when they took place.

Furthermore, OIML D 31 requires that the integrity of software and the correctness of parameters be verified during verification of measuring instruments. When a measuring instrument is equipped with an audit trail, the verifier may examine the audit trail to review the history of operations and interventions recorded in the instrument and assess whether the instrument has been operated in compliance with the applicable requirements.

2. Proposed Framework: Audit Trail Check Using Runtime Verification

Runtime verification (RV) is a formal verification technique used to determine whether an event sequence obtained during the execution of a computing system satisfies a given specification [2, 3]. Here, a specification describes the required behaviour of the system, typically in the form of logical formulae. By evaluating the observed event sequence against the specification, it is possible to determine automatically whether the system exhibits the required behaviour.

Given the characteristics described above, RV has been regarded as a suitable technique for audit trail checks. An audit trail consists of a time-ordered sequence of events occurring within a measuring instrument, such as parameter changes and software updates. By evaluating the audit trail against prescribed specifications, it is possible to determine formally whether the recorded behaviour conforms to the specified requirements.

To automate audit trail checks, a framework based on RV was proposed [4]. Figure 1 shows a schematic diagram of the framework. The framework consists of three elements: an audit trail, check formulae, and an RV tool. The audit trail is a sequence of events occurring within a measuring instrument, while the check formulae are logical formulae that formally represent requirements derived from OIML D 31.

The RV tool evaluates each check formula against a given audit trail and outputs a truth value, either true or false, indicating whether the formula is satisfied. This makes it possible to determine systematically whether the audit trail satisfies the individual requirements. The final result of the audit trail check is determined on the basis of the obtained set of truth values. If all check formulae evaluate to true, the audit trail check is classified as Pass. Conversely, if at least one check formula evaluates to false, it is classified as Failure.

Figure 1. Schematic diagram of the proposed framework of the audit trail check using runtime verification.

3. Demonstration of Audit Trail Check Based on the Framework

Based on the framework described in the previous section, a demonstration was conducted to illustrate the proposed method for audit trail checks [5, 6]. An overview of the demonstration is presented below.

First, a non-automatic weighing instrument was selected as the target of the demonstration. In reference [5], a simplified design of a non-automatic weighing instrument was proposed for the scope necessary for the demonstration. In this design, events that may occur within the measuring instrument, such as parameter changes, mode transitions, and software updates, were defined. These events need to be recorded so that the conformity of a measuring instrument with applicable requirements can be assessed through an audit trail check. Examples of the events selected for recording are shown in Table 1. In the design proposed in reference [5], these events are identified and specified in a recordable format together with the information required for conformity assessment.

Next, check formulae for audit trail were derived. In reference [4], the requirements specified in OIML D31 were organized as abstract formal specifications. In reference [5], these abstract formal specifications were instantiated based on the design of the target non-automatic weighing instrument and the corresponding audit trail design. As a result, check formulae were derived for the target non-automatic weighing instrument. To express the check formulae, first-order temporal logic [7, 8], a mathematical logic capable of describing temporal relationships between events, was employed. The resulting check formulae describe properties such as the occurrence of some events only under specified conditions (e.g., a parameter change is permitted only when the instrument is in maintenance mode), the occurrence of events in a prescribed order (e.g., a software update shall be performed only after user consent has been obtained), and the absence of particular events (e.g., a legally relevant parameter such as gravitational acceleration shall never be modified).

As an example of a check formula, a formula expressing the property that the parameter “Zero AD” shall not be modified is considered. Here, Zero AD denotes the output value of the A/D converter when the non-automatic weighing instrument is in the unloaded state. Modifying this value affects the metrological characteristics of the instrument. The corresponding check formula, expressed in first-order temporal logic, is shown in (1):

(1)

Here, G is one of the temporal operators in first-order temporal logic. When written as Gφ, it means that the formula φ holds at all future points in time. In addition, ¬ denotes logical negation. Since the condition

evaluates to true whenever the parameter “Zero AD” is modified, (1) states that no event modifying “Zero AD” occurs throughout the audit trail.

Furthermore, based on the design of the non-automatic weighing instrument, multiple operational scenarios were defined, and audit trails simulating the behavior of the instrument in those scenarios were generated. Examples of such scenarios include a software update being performed without user consent and the modification of the parameter “Zero AD”, whose integrity must be maintained. A fragment of the audit trail corresponding to the latter scenario is shown in Listing 1. In this fragment, each entry consists of a timestamp represented in Unix time and the corresponding recorded events. In the second entry, a modification of the parameter “Zero AD” is recorded, thereby violating Formula 1.

The generated audit trails were evaluated against the check formulae using Monpoly [9, 10], an existing RV tool. As a result, audit trails satisfying the requirements were classified as Pass , whereas audit trails containing violations were classified as Failure. This demonstration shows that, for the prepared audit trails, the framework can correctly distinguish between scenarios that satisfy the requirements and those that violate them. These results are consistent with the expected outcomes and illustrate how the proposed framework can be used to assess the conformity of measuring-instrument behavior based on audit trails.

Table 1. Examples of events recorded in the audit trail of a non-automatic weighing instrument.

Listing 1. Fragment of an audit trail containing a modification of the parameter “Zero AD”.

@1696554500  moveMaintenanceMode()
@1696554532  changeParameterInt(success, Zero AD, 450, 534, calibration)
@1696554560  shutdown()

4. Conclusions

This article introduced the framework for checking audit trails using runtime verification as a means of ensuring the reliability of measuring instruments in legal metrology. In the proposed framework, properties derived from the requirements specified in OIML D 31 are expressed as check formulae. By applying these check formulae to audit trails, it is possible to determine whether the operation of a measuring instrument conforms to the specified requirements.

A demonstration has already been conducted based on the design of a non-automatic weighing instrument equipped with an audit trail function. Through concrete examples of check formulae and simulated audit trails generated from the design, the demonstration showed that audit trails conforming to the requirements were classified as Pass, whereas audit trails containing violations were classified as Failure.

These results indicate that, for the audit trails considered in the demonstration, the proposed framework was able to distinguish between those behaviours that satisfied the requirements and those that violated them. As software continues to play an increasingly important role in measuring instruments, audit trail checks performed in accordance with the proposed framework may provide an effective approach for ensuring the proper operation of measuring instruments in legal metrology.

References

[1] OIML D 31:2023 General requirements for software controlled measuring instruments (available from www.oiml.org/en/publications/documents/)

[2] Bartocci E et al 2018 Introduction to runtime verification Lect. Notes Comput. Sci. 10457 1–33

[3] Leucker M and Schallhart C 2009 A brief account of runtime verification J. Log. Algebr. Methods Program. 78 293–303

[4] Hiroshi W 2022 Specification for audit trail in OIML D 31: toward runtime verification IMEKO TC6 Int. Conf. on Metrology and Digital Transformation (available at: www.imeko.org/publications/tc6-2022/IMEKO-TC6-2022-019.pdf)

[5] Okamoto J 2025 Demonstration of checking an audit trail for a measuring instrument using runtime verification Meas. Sci. Technol. 36 036207

[6] Okamoto J 2026 Use of runtime verification for audit trail check in remote verification of measuring instruments Meas. Sci. Technol. 37 216201

[7] Chomicki J 1995 Efficient checking of temporal integrity constraints using bounded history encoding ACM Trans. Database Syst. 20 149–86

[8] Lima L et al 2024 Explainable online monitoring of metric first-order temporal logic Lecture Notes in Computer Science 288–307

[9] Basin D et al 2012 MONPOLY: monitoring usage-control policies Lect. Notes Comput. Sci. 7186 360–4

[10] Basin D et al 2017 The MonPoly monitoring tool RV