[L]This work has been submitted to the IEEE for possible publication.
Copyright may be transferred without notice, after which this version may no longer be accessible.

The safety of automated driving systems must be justified by convincing arguments and supported by compelling evidence to persuade certification agencies, regulatory entities, and the general public to allow the systems on public roads. This persuasion is typically facilitated by compiling the arguments and the compelling evidence into a safety case. Reviews and testing, two common approaches to ensure correctness of automotive systems cannot explore the typically infinite set of possible behaviours. In contrast, formal methods are exhaustive methods that can provide mathematical proofs of correctness of models, and they can be used to prove that formalizations of functional safety requirements are fulfilled by formal models of system components. This paper shows how formal methods can provide evidence for the correct break-down of the functional safety requirements onto the components that are part of feedback loops, and how this evidence fits into the argument of the safety case. If a proof is obtained, the formal models are used as requirements on the components. This structure of the safety argumentation can be used to alleviate the need for reviews and tests to ensure that the break-down is correct, thereby saving effort both in data collection and verification time.

Automated driving, formal methods, safety case, system engineering, precautionary safety, risk norm

§ INTRODUCTION

Automated Driving Systems (ADS) relieve the human driver from the driving task and let the driver engage in other activities while travelling [SAE J3016`_202104, 2021]. Among several potential benefits of ADS, one in particular is to prevent accidents caused by driver errors and thereby increase traffic safety [EU:, 2019]. An indication that such potential traffic safety benefit exists is provided by extrapolation from previous experience with driver assistance systems [Eugensson et al., 2013], and by analyses showing that ADS have the potential to prevent or reduce the severity of several accident scenarios involving human drivers [Lubbe et al., 2018]. However, these studies only apply to situations that human drivers do not handle safely, and accidents involving human drivers; they do not provide insights into situations that human drivers already handle safely.

ADS are designed to take over operation of the Dynamic Driving Task (DDT) in environments that are included in a specific Operational Design Domain (ODD) [SAE J3016`_202104, 2021]. To provide a net increase in traffic safety, an ADS must perform the DDT such that it overall is safer than a human driver in all the environments of the ODD. It must also limit operation to environments included in the ODD, or risk unsafe behavior.

As human drivers in general have a very low failure rate [Kalra and Paddock, 2016] and as the ADS cannot expect human supervision or intervention in its ODD, the ADS becomes highly safety critical.

Two pertinent problems arise when developing these safety-critical ADS: [label=(*)]

* the development methods and processes that are applied must ensure safety of ADS [Koopman and Wagner, 2017], and

* this fact must be supported by compelling evidence to persuade certification agencies, regulatory entities, and the general public of the safety of ADS. In essence, safety of the ADS must be demonstrated, rather than assumed until proven unsafe [Koopman et al., 2019].

ADS have a bidirectional interaction with their surrounding environment; that is, an ADS must adapt its behavior to the environment, and the environment behavior is affected by the ADS's actions. This paper considers ADS that can be represented by an architecture with three components as shown in  <ref>. The component senses and perceives the environment, the component is responsible for decisions on when and how to act, and the component executes the decisions using the respective actuators. These components interact with the environment, here represented by the ODD, in a feedback loop.

block/.style=rectangle, draw, text width=4.5em,
text centered, rounded corners, minimum height=2.3em,

[block] (sense) ;
[block,right=0.5cm of sense] (dc)  ;
[block,right=0.5 cm of dc] (act)  ;
[block, below=0.4 cm of dc] (odd1) odd;
[draw, thick, dashed, fit=(sense) (dc) (act), inner xsep=0.85 cm, inner ysep=0.22 cm, label=ADS] (temp) ;

[arrow] (sense) – (dc);
[arrow] (dc) – (act);
[arrow] (act.east) -| ($(act.east)!.5!(temp.east)$) |- (odd1.east);
[arrow] (odd1.west) -| ($(sense.west)!.5!(temp.west)$) |- (sense.west);

A simplified architecture for an ADS.

The feedback loop between an ADS and its environment means that compelling safety evidence must be gathered in closed-loop conditions, and the compiled evidence must be shown to be representative of all the environments in the ODD. One way to accomplish both of these points is to perform real-world driving that covers the entire ODD, and drive enough distance such that safety can be evaluated. However, testing in real-world driving conditions as the only means for aiding safety-critical development and producing compelling evidence for safety is infeasible for all but trivial ODDs [Kalra and Paddock, 2016, Koopman et al., 2019, Koopman and Wagner, 2016].

To overcome this obstacle, the process of evidence collection often follows a divide-and-conquer approach. This is done by first breaking down the system-level ADS requirements to its components, and then further to smaller elements until the effort to support each requirement with compelling evidence is acceptable [ISO/PAS 21448:2022, 2022, ISO 26262:2018, 2018]. A benefit of this approach is that the evidence can be collected by methods that are specialized for the specific type of requirement, but which may not be feasible for system-level requirements. A drawback, however, is that fulfillment of the component-level requirements must now imply the fulfillment of the system-level requirements in the entire ODD. To ensure that there are no gaps in the broken-down requirements, verification must still be performed for the complete ADS, but to a lesser extent.

Reviews and Testing are two often recommended methods to ensure correctness of electronic automotive features [ISO 26262:2018, 2018]. Both of these methods are used to find faults or insufficiencies

the development process. They are complementary and often find different kinds of issues. However, neither is exhaustive, mainly because reviews are laborious, and because testing cannot explore the typically infinite set of possible behaviors in its entirety. These challenges are exacerbated for feedback systems, especially when discrete decisions are taken, and when errors take long time to propagate into failures. For instance, to avoid collisions with pedestrians, an ADS must approach road-side pedestrians with a suitable speed so that it can guarantee to stop safely, should the pedestrian step out into the road. A bad decision by the ADS can cause a collision several seconds or minutes later; deciding to pass the pedestrian although it is too close to the road will erroneously remove the braking option, but this error will not become apparent until, and if, the pedestrian enters the road.

Formal methods are a category of methods that can prove and ensure correctness of feedback-system models with respect to the requirements. In contrast to testing, these methods are exhaustive and provide evidence that no faults or insufficiencies are present in the component model, at least not w.r.t. the specified behaviour. They are also automatic or semi-automatic, so they typically require less labor than reviews.
This paper shows how formal methods can be used to justify that components relying on feedback fulfill their requirements, and thereby give compelling evidence for the safety of the component. Furthermore, this paper demonstrates how formal methods can be used to close the gap between the ADS system requirements and the broken-down component requirements. This is done by showing how the formalization of the system-level safety requirements of the ADS puts assumptions and verification conditions on the different components, and on the ODD. The assumptions thus obtained also give a formal description of the conditions that must be fulfilled for the formal proof to be valid, and this paper puts forth an argument that those conditions in certain instances may be evaluated in open-loop settings, thereby considerably decreasing the verification effort. Both the above contributions are illustrated and argued based on a relevant example from the industry.

§ RELATED WORK

lists formal methods as techniques for ensuring dependability on the software architectural and unit design level [ISO 26262:2018, 2018].

At these levels, the software is typically considered as open-loop input/output systems, and this is also the intended setting in the standard. In this context, formal methods can provide evidence that the software is dependable [Denney et al., 2012]. Formal methods are not considered at other levels of the design in the standard, and hence there are no recommendations regarding formal methods applied to feedback systems.

Formal methods have been used successfully in the automotive domain to prove that complex feedback systems are correct with respect to safety in a given environment [Loos et al., 2011, Nilsson et al., 2012, Wongpiromsarn et al., 2013, Korssen et al., 2018, Selvaraj et al., 2022, Krook et al., 2019]. However, these works do not demonstrate how the artifacts from the formal methods contribute to a convincing argument that safety is achieved.

Previous research has established that there are opportunities for using evidence from formal methods to convincingly argue for safety in all levels of the design of safety-critical systems [Galloway et al., 2008, Rushby, 2010]. Moreover, it is argued that the assumptions on the environment are an important part of the model, and their inclusion allow more focus on the evidence and validation instead of ensuring that the break-down of requirements is correct [Galloway et al., 2008, Rushby, 2010]; an argument which is supported by the contributions in  <ref>. There is also a challenge in how to treat probabilistic requirements when employing formal methods [Rushby, 2010], which is also addressed in  <ref>.

When using formal methods to argue that a system is safe, it is imperative that both the underlying formalism and the tools that are being used are correct. Obviously, there must be a convincing argument that this is indeed the case, but such argument is out of scope of this paper as it is typically available from literature associated with the respective methods. There are many aspects to consider with respect to the correctness of the formalism and any tool being used, and a generic argument that captures all these aspects is provided by  [Habli and Kelly, 2009].

§ SAFETY CASE

A safety-critical system, such as an ADS, must behave such that safe operation is ensured in its entire ODD, where, commonly, safe is taken to mean that there is an absence of an unreasonable risk of harm. When a safety-critical ADS is developed, it must be ensured that its behavior indeed is safe, but it must also be justified by compelling evidence that the risk of harm is low enough. This latter part is required to persuade certification agencies, regulatory entities, and the general public.

The justification of an ADS's safety can be compiled into a safety case, which is a structured argument, supported by a body of evidence that provides a compelling, comprehensible and valid case that a system is safe for a given application in a given operating environment [Ministry of Defence, 2017]. There are three principal elements in a safety case: requirements, arguments, and evidence [Kelly and Weaver, 2004]. The safety case approach has been used in many safety critical industries to demonstrate safety, and is also recommended by automotive safety standards such as the  [ISO 26262:2018, 2018] and  [ISO/PAS 21448:2022, 2022].

Since a safety case is used to demonstrate that a product is safe, it is imperative that its structure is clear, comprehensible, and accurate. The Goal Structuring Notation (GSN) is a standardized graphical argument notation [Kelly and Weaver, 2004, ACWG, 2021], which can be used to structure a safety case. It explicitly documents the individual elements of a safety argument and their relationships to the gathered evidence. GSN defines core elements, two types of relationships between the core elements, and an undeveloped element decorator, as shown in  <ref>. The two relationships SupportedBy and InContextOf declare a relationship between a source element and a target element. The elements are linked together in a logical structure known as the GSN goal structure, which is a directed acyclic graph. The top-level goal in a goal structure is gradually refined through a series of more detailed goals until a direct link to evidence is made [Kelly and Weaver, 2004]. The undeveloped element decorator indicates that a line of argument has not been developed in the current context.

[GSNsolution, inner sep=0.025cm] (solution)   Solution$\langle$description$\rangle$;
(cnw) at (solution.north -| solution.west);
[GSNstrategy, left=1.25cm of cnw, anchor=north east] (strategy) Strategy $\langle$description$\rangle$;
[GSNgoal, left=of strategy] (goal) Goal$\langle$description$\rangle$;
[GSNassumption, below=1.25cm of goal.south west, anchor=west, inner sep=0.05cm] (assumption) Assumption$\langle$description$\rangle$;
[GSNcontext, right=0.5cm of assumption] (context) Context$\langle$description$\rangle$;

[right=0.5cm of context] (temp);
[below=0.1cm of temp] (i1);
[right=of i1] (i2);
[below=0.5cm of i1] (i3);
[right=of i3] (i4);
[GSNsupportedBy](i2) – (i1);
[GSNcontextOf](i4) – (i3);
[GSNundeveloped, right=0.75cm of i2, anchor=north] (undeveloped) ;

The core elements of a GSN goal structure. The line with a solid arrowhead denotes a

relationship and the line with the hollow arrowhead denotes an

relationship. The diamond indicates an undeveloped element.

§ FORMAL METHODS

Formal methods are a class of mathematically rigorous techniques and tools used to specify, design, verify, and synthesize components, mainly by mechanizing rigorous reasoning about correctness of these components [NASA, 2016]. As such, the field is very broad, and a wide plethora of tools are available for many different parts of the development process and at different levels of abstraction. This paper is concerned with formal methods applied to the function layer of the ADS, i.e., details of the hardware and the software are abstracted away.

Formal methods are based on languages with formal syntax and semantics that leave no room for ambiguity. Common to all classes of formal methods is that a requirement on the system, in this case an ADS, is formalized into a specification that details correct behavior of the system. In the case of input/output systems, the formal specification relates the required output to certain input, but in this paper the specification details the allowed behavior over time for feedback systems.

Since the safety requirements for an ADS describe disallowed and mandated behaviors over time, logical formalisms that support modelling and reasoning about properties with respect to time, such as Linear Temporal Logic (LTL) [Baier and Katoen, 2008] and differential dynamic logic () [Platzer, 2018], are typically used to formalize the requirements. Often safety requirements are characterized as nothing bad shall happen [Baier and Katoen, 2008], which is easily formalized using the modal operators to describe necessity in LTL and in . For instance, $\Box \phi$ in LTL asserts that the property $\phi$ always holds and $[\mdl]\phi$ in asserts that after all behaviours of model $\mdl$, the property $\phi$ holds.

Given such a formal specification, formal verification and formal synthesis provide evidence of correctness of formal models of feedback systems in the form of a machine checked formal proof of the fulfillment of the specification. For formal verification, all parts in  <ref>, and their possible interactions, are modelled in a formal language, and then the formal verification tool attempts to prove that the formal model fulfills the formal specification. For formal synthesis, the goal is instead to automatically construct, typically, a model of such that the resulting feedback system is guaranteed to fulfill the formal specification. In the case of synthesis, the models of , , and the ODD are commonly referred to as the assumptions, whereas the required behavior of the feedback system is referred to as the guarantees. This distinction is not as common in the case of formal verification, but in this paper the modelled parts will be referred to as the assumptions of the system regardless of method.

§ PROPOSED SAFETY ARGUMENT APPROACH

For feedback systems like ADS, the break-down of requirements onto components can be difficult since requirements on the system-level refer to behaviors of the closed-loop system in the context of the ODD, whereas the component requirements specify the behavior at the interfaces between the components. The fulfillment of the component requirements must imply the fulfillment of the system requirements; if this is not the case, there is either a behavior disallowed by the system requirements that is allowed by the component requirements, or there is a behavior mandated by the system requirements that is not mandated by the component requirements. When the involved requirements are safety critical, this potential discrepancy between the behaviors that are disallowed or mandated at different levels might lead to an unsafe ADS. Compelling evidence that this potential discrepancy does not decrease the safety to an unacceptable level must be dealt with in the safety case [ISO 26262:2018, 2018, Bergenhem et al., 2015].

The approach in this paper uses formal methods to prove that the break-down has no such discrepancy. The system requirement is formalized into a guarantee to be fulfilled, and the formal system model is composed of the formal models of the components and the ODD. The approach is to use these models as specifications for the components. The component specifications can be developed into formal contracts [Sangiovanni-Vincentelli et al., 2012] that provide unambiguous requirements for the separate components. By this decoupling, specialized methods can be used to develop and verify the broken-down requirements. Hence, if the guarantee is proven to be fulfilled by the formal models, and if the verification of the components indicate that they fulfill their formal specifications, then the system requirement is fulfilled in the ODD, and there is compelling evidence for this fact in the form of a formal proof.

For instance, the guarantee could be a formalization of there are no impacts with pedestrians. Likely, for the ADS to fulfill this guarantee, the component must be able to provide some deceleration below some minimal level. More specifically, assume that the component requests an acceleration $\areq$ in a certain range, then must ensure that the true acceleration $a$ of the vehicle fulfills $a \leq \areq$. Then the property $a \leq \areq$ is considered the specification for the component.

In the case that the system requirement is quantitative, specifying a probability or an occurrence rate of an event, then the formal guarantee is specified such that the event must not occur. In the break-down process, the models of the components are assigned a probability or occurrence rate with which they may be violated, such that the cumulative violations of the assumptions in the formal model does not exceed what is allowed by the system requirement.

The approach is illustrated in  <ref> with an example where a safety requirement with respect to pedestrians is broken down to safety requirements on the closed-loop system. It is then shown how the artifacts of the formalization of these requirements can be used to structure an argument in a safety case. The argument is illustrated graphically by a GSN goal structure in  <ref> to make the relations between requirements and arguments clear.

§ PRECAUTIONARY SAFETY AND RISK NORM

The example in this paper is based on the concept of Precautionary Safety (PCS) [Rodrigues de Campos et al., 2021]. PCS attempts to ensure safety by adjusting an ADS's behavior based on its capabilities, external conditions, and expected exposure to incidents. The notion of safety in this context follows the concept of Quantitative Risk Norm (QRN) [Warg et al., 2020], where certain accident types with certain severity (in terms of human injury) are assigned a minimum allowed mean time between accidents (risk norm). Based on an assessment of Swedish national accident injury data for pedestrians and an estimation of total hours driven, an acceptable mean time between accidents

can be established. The severity is highly correlated with impact speed [Peden et al., 2004], so the allocated risk norms are in  <ref> given based on impact speed.

Risk Norms for Pedestrians. Different Mean Time Between Failures for Different Accident Severities.

Impact speed
[km/h]     Risk norm [h]

$<$ 10     100 000

$[10, 20)$     1 000 000

$[20, 30)$     10 000 000

$[30, 40)$     100 000 000

$\geq$ 40     1 000 000 000

The ADS is intended to operate up to a speed of 70km/h on urban roads, and up to 100km/h on highways, so these are the environments that make up the ODD. The allowed failure rate of the ADS depends both on the risk norm and on the incident exposure rate in the ODD, i.e., the mean time between the occurrence of pedestrians. This exposure rate is different for different road segments, as pedestrians are more likely to appear on the road in low-speed urban settings than on highways with free-flowing traffic. The assumed exposure rates for urban and highway driving are given in  <ref> (c.f. [Rodrigues de Campos et al., 2021] [Rodrigues de Campos et al., 2021]).

Exposure Levels with Respect to Speed and Road Type

Speed     2cExposure [h]

[km/h]     Urban Roads     Highways

30     100     100 000

50     1 000     1 000 000

70     10 000     10 000 000

100     -     10 000 000

The QRN argument that the ADS feature is sufficiently safe with respect to pedestrians is illustrated graphically by the goals G1, G2, and G3 in  <ref>. G1 represents the top-level safety requirement that the ADS feature shall be safe with respect to pedestrians. G1 is then made more specific in G2 by relating safety to its definition of having sufficiently high mean time between accidents. G2 is fulfilled via the strategy S1, which argues that the ADS is sufficiently safe whenever the risk norms in  <ref> are fulfilled, as exemplified by G3. Note that the four goals corresponding to the other risk norms in parallel to G3 are not shown. G3 is broken down based on exposure level, corresponding to the different road types. Each combination of exposure level and risk norm gives rise to an impact probability per event, where the maximum allowed impact probability in is calculated by the ratio of exposure and risk norm. Not shown in parallel to in the branch rooted in G3 are the six other exposure classes from  <ref>. All other goals in parallel to G3 are supported by an analogous argument structure. This paper and the PCS paper
[Rodrigues de Campos et al., 2021]
agrees on the safety case so far, but differs below .

GSN illustrating the argument made in this paper. A bigger version is available at <https://doi.org/10.5281/zenodo.7142341>.

In [Rodrigues de Campos et al., 2021] [Rodrigues de Campos et al., 2021], an already implemented reactive collision-avoidance module's capability to avoid collisions by braking is determined in simulations. The capability is presented as the probability of a certain impact speed given the speed before braking starts. The mean time between certain impact speeds for certain roads is then calculated as the ratio of the exposure on that road and the probability of that impact speed given the speed of the road. The mean time between impact speeds is then compared to the QRN to determine the maximum allowed speed that the ADS may drive on that road; if the mean time between accidents of a certain impact speed for a certain initial speed is lower than the QRN, then the ADS may not drive that fast on that road. For instance, exposure on urban roads with speed 70km/h is 10 000h, and the probability of an impact speed of 1020km/h for a speed of 60km/h is 5. The ratio is 200 000h, considerably less than the QRN of 1 000 000h, so the ADS cannot be allowed to drive at 60km/h on urban roads with a speed of 70km/h. Thus, safety is ensured by taking precaution; the maximum speed is adapted based on the expected capability of mitigating impacts and the exposure to incidents.

However, this way of applying the PCS concept assumes an already implemented ADS. If it is desired to drive at 70km/h on urban roads, PCS indicates that the probability of impact speeds of 1020km/h ought to be at most 1. One way of reaching such performance would be to iteratively implement improvements and simulate and test until the capability is sufficiently safe for driving at 70km/h. This paper shows how formal methods can be used to instead break down the requirement to components to achieve a systematic development process. It is also shown how the break-down through formal methods helps with structuring an argument supporting the fulfillment of the safety case.

The main idea of PCS still applies; the ADS ought to take precaution by considering what might happen, not solely what is happening, to avoid unacceptable risk of harm. Formal methods explore the entire state space of the formal model in order to prove the guarantee, so they fit well as a tool to ensure that all possible events are considered by the ADS.

§ FORMAL METHODS IN THE SAFETY CASE

To ease the development effort, the goal in  <ref> may be broken down to , , and that are assigned to the respective components in  <ref>, and in that way separate the concerns for design and verification of the different components. This is a typical way to combat complexity by allowing application of specialized tools and methods to the design and verification of the components [ISO 26262:2018, 2018, Sangiovanni-Vincentelli et al., 2012]. As stated earlier, these components' goals must imply the goal in  <ref> lest the risk of harm may be unacceptable.

Formal methods can provide proofs as evidence that, in the context of the ODD, the component models fulfill the guarantee. However, the guarantee is a qualitative logical formula, whereas is a quantitative goal with a probability. To deal with this, the strategy for fulfilling is split into one qualitative part and one quantitative part, as can be seen in  <ref> where is supported by the two strategies and . The idea here is to disregard the probability in and formalize the remainder as the guarantee, and then find a formal model that satisfies that guarantee. To reintroduce the probability, it is finally argued that the goal is fulfilled as long as the assumptions in the formal model are violated with at most the same probability as in .

The entire argument hinges on the correctness of the formal model with respect to the guarantee, and this is captured by . It is made explicit with the context relation that the formal model is composed of the assumptions on the ODD and the models of the components , , and , and the guarantee which correctness is evaluated against. The sole evidence that is fulfilled is provided by the machine checked formal proof.

Now assume that the behavior of the components , , and fulfill their corresponding formal assumptions with probabilities such that the entire formal model is fulfilled with a probability of at least 0.99. Then is fulfilled because the guarantee that “no impacts occur” is violated at most with a probability of 0.01, which in turn means that impacts in the range 010km/h can occur at most with a probability of 0.01.

Therefore, is broken down into , , and , each detailing the probability of the assumed behaviors of , , and , respectively, are being violated. Here, the probabilities are assigned arbitrarily, but it is ensured that their sum

does not exceed the probability of . It can be argued via strategy that the break-down of to , , and is correct, and it can be argued via strategy that is fulfilled because , , and are fulfilled. The component models can serve as formal specifications for the individual components, and relevant standards may be used to develop and verify the three components according to these specifications [ISO/PAS 21448:2022, 2022, ISO 26262:2018, 2018].

To be a bit more specific, it is now illustrated with more detail what the context of may look like.

Since the intention is to show how a formal-methods approach could be used in the safety case and not discuss any specific formal method in detail, the approach in this paper is illustrated with abstract artifacts and simple models for the three components in  <ref>. The first type of artifact, the guarantee <ref>, is the formal specification based on .

There are no impacts with pedestrians.

<ref> can be formalized in different ways depending on the formalism used. For example, <ref> can be formalized in LTL using the formula $\Box \lnot \predcoll$ where is a predicate describing the undesirable property of the occurrence of an impact; and in using the formula $[\mdl](\lnot \predcoll)$, where  is the formal model.

Irrespective of the formalism used, formal models of the components are required in order to either synthesize a controller that guarantees <ref> or verify that a given design fulfills <ref>. Thus, the second type of artifact is formal models of the ADS components in  <ref>. As for the formal specification, the ADS components can be modelled in different ways depending on the formalism of choice.
To formalize the components, parameters about the ADS vehicle and pedestrians are considered, as shown in  <ref>.

Parameters Considered in the ADS Model

Parameter     Description

$x$, $v$, $a$      position, velocity, acceleration of ADS vehicle

,      minimum, maximum acceleration of ADS vehicle

$\delta$     actuator disturbance

,     true position, lateral velocity of pedestrian

,      estimated position, lateral velocity of pedestrian

$\epsilon$     sensor disturbance

This paper considers a component with a safety controller such as the one in [Selvaraj et al., 2022] [Selvaraj et al., 2022] to guarantee safety. For the sake of brevity, <ref> presents a very abstract model of . The required acceleration is set to the minimum acceleration if the predicate $\lnot \safe$ is satisfied. This predicate can be used to describe decision-making conditions such as checking if there is some choice of $\areq \in [\amin, \amax]$ such that, later on, stopping before the pedestrian is infeasible.

[] $\quad\lnot \safe \to \areq = \amin$

Of course, to prove that <ref> fulfills <ref>, certain assumptions must be made on the other components. Typically such assumptions are identified as a result of the formal modelling and analysis. In this context,

consider <ref>, <ref>, and <ref> as the assumptions on the ODD, , and , respectively. The assumption on the ODD describes that the ADS vehicle velocity $v$ is non-negative, and it defines the limits on pedestrian velocity $\vp$.

[] $\quad v \ge 0 \land 0 \le \vp \le 10$

The range of allowed values for $\vp$ defines what may happen in the environment, and the exhaustiveness of formal methods make sure that all different combinations with all different timings are evaluated. A controller that fulfills the requirement in the presence of $\vp$ certainly takes precaution for what might happen, and not only reacts to what is happening.

<ref> describes that, if the true position $\xp$ of the pedestrian is within the detection range of the sensor, then the error in the estimated position of the pedestrian $(\hatxp - \xp)$ is at most $\epsilon$. Furthermore, if $\xp$ is in front of the ADS vehicle, then $\hatxp$ is also estimated to be in front.

\begin{equation*}
\left(\xp \le \range \to \hatxp - \xp \leq \epsilon\right)\, \land\, \left(\xp \ge x \to \hatxp \ge x\right)
\end{equation*}

The tolerances make it possible to assign probabilities to the fulfillment of the specifications. The exhaustiveness of formal methods evaluates all combinations, so the exact probability distribution does not need to be known.

The assumptions on the described by <ref> state that if the requested acceleration is within the bounds, then the tracking error tolerance between actual acceleration and requested acceleration is at most $\delta$.

[] $\quad
\amin \le \areq \le \amax \to a \le \areq + \delta $

Assume that the formal model  composed by <ref> – <ref> is correct with respect to the guarantee <ref>, and that there exists a formal proof that this is indeed the case. The proof provides enough evidence that in  <ref> is fulfilled.

For to be fulfilled, the realized controller in the component must fulfill the behavior specified by <ref>. This may be assured, for instance, by following the recommendations in  [ISO 26262:2018, 2018] to achieve a fault tolerant realization. Since <ref> is a simple condition relating inputs to outputs, much of its verification can be performed in open loop, which results in less effort to collect evidence that is fulfilled.

This paper does not consider strategies to validate the ODD, so in A1 in  <ref>, <ref> is considered an assumption in the argument, which means that there is no justification or evidence that <ref> is fulfilled. Obviously, to ensure real-life safety, this assumption must be validated for the roads that the ADS vehicle is allowed to drive on. That endeavor may benefit greatly from having a formalized formulation of assumed properties of the ODD.

The model <ref> specifies the required behavior of for the guarantee to be fulfilled, and details the probability with which this behavior may be violated. This requirement can, to a large extent, be verified in open loop on recorded data, provided that the behavior in the recordings adhere to the assumptions of <ref>. This could provide a substantial benefit since the data may be collected before all components are realized, and because the recorded data is still relevant after implementation has changed in the components. This is not the case for the approach by [Rodrigues de Campos et al., 2021] [Rodrigues de Campos et al., 2021] when assessing the capability of the complete vehicle. Furthermore, the verification of does not need to ensure that there are enough outcomes with different impact speeds, as the requirement is independent of the closed-loop outcome. This last point can potentially save effort both in data collection and verification time.

The last model, <ref>, which specifies the acceleration tracking performance, must still be verified in closed-loop conditions. However, the break-down of requirement into makes the verification independent of the other components, which may simplify the verification method. To realize and below the goals and , the development process could, for instance, employ  and .

§ DISCUSSION

The approach in  <ref> is one possible argument structure to include formal proofs of correctness as evidence in safety cases. Whether the approach is beneficial depends on the overhead of the formal methods in comparison to the verification effort, and as such, the approach may be beneficial for some systems, and not for others, and it might be beneficial for only a subset of the requirements in one system.

The benefits are also dependent on the formal modelling and the system decomposition. Some system decompositions may not be possible to formally model in a given formalism, and the formal specifications of a component might fail to be verifiable, or exceedingly hard to verify. Such complications will trigger redesigns that could be costly.

On the other hand, a notable benefit is that the presented approach in itself is agnostic to the chosen methods and technologies with which the components are realized. Admittedly, some might be more amenable to be used in conjunction with the formal specifications.

Furthermore, if formal methods are employed at an early stage in the project, they may catch inconsistencies and design flaws that would be costly to find during system-level testing. The process of formalization of requirements can itself be beneficial, and the approach detailed in this paper allows more utilization of such work.

The proposed approach uses a strategy to split a quantitative goal into one qualitative and one quantitative part. The qualitative part disregards the probabilities involved and employs formal methods to provide evidence to show that the qualitative part is fulfilled. However, there exists formal approaches that can prove correctness of stochastic systems such as probabilistic model checking [Kwiatkowska et al., 2022] where quantitative extensions of temporal logic are used to specify quantitative properties. While it is beneficial to investigate the suitability of such approaches to provide evidence to quantitative goals in the safety argument, they are not considered in this paper.

§ CONCLUSIONS

This paper presents an approach to structure the safety case for employing formal methods in safety cases for automated driving systems. The artifacts from the formal analysis are used as formal specifications on the components of the system, thus providing a break-down of safety requirements to individual components. The formal proof provided by the formal method is used as evidence that the break-down is correct. If the safety requirement specify a quantitative target, then this is handled by assigning quantitative targets for the specifications on the components, in parallel to the formal model.

This approach gives several potential benefits by limiting the effort of safety assurance, and by breaking down requirements on a complex system into well defined and unambiguous specifications on individual components. First of all, less effort is needed to verify that the break-down of the requirement is correct, as this is proven by the formal method. Second, the formal specifications on the components provide separation of the concerns, and may also allow for verification in open-loop settings instead of closed-loop settings for some components, which leads to more flexibility and less effort to verify the individual components. Case studies of complex systems are needed to validate this approach.

[SAE J3016`_202104, 2021]
SAE J3016`_202104, “Taxonomy and definitions for terms related to
driving automation systems for on-road motor vehicles,” SAE Int., Tech.
Rep., Apr. 2021.

[EU:, 2019]
“Regulation (EU) 2019/2144 of the European Parliament,” url:
<http://data.europa.eu/eli/reg/2019/2144/oj>, Dec. 2019.

[Eugensson et al., 2013]
A. Eugensson, M. Brännström, D. Frasher, M. Rothoff, S. Solyom, and
A. Robertsson, “Environmental, safety, legal and societal implications of
autonomous driving systems,” in Int. Tech. Conf. Enhanc. Saf. Veh.,
vol. 334, 2013.

[Lubbe et al., 2018]
N. Lubbe, H. Jeppsson, A. Ranjbar, J. Fredriksson, J. Bärgman, and
M. Östling, “Predicted road traffic fatalities in germany: The potential
and limitations of vehicle safety technologies from passive safety to highly
automated driving,” in Int. Res. Counc. Biomech. Inj., Sep. 2018, pp.

[Kalra and Paddock, 2016]
N. Kalra and S. M. Paddock, Driving to Safety: How Many Miles of Driving
Would It Take to Demonstrate Autonomous Vehicle Reliability?1em plus
0.5em minus 0.4emRAND Corporation, 2016.

[Koopman and Wagner, 2017]
P. Koopman and M. Wagner, “Autonomous vehicle safety: An interdisciplinary
challenge,” IEEE Intell. Transp. Syst. Mag., vol. 9, no. 1, pp.
90–96, Jan. 2017.

[Koopman et al., 2019]
P. Koopman, A. Kane, and J. Black, “Credible autonomy safety argumentation,”
in 27th Saf.-Crit. Syst. Symp., Feb. 2019.

[Koopman and Wagner, 2016]
P. Koopman and M. Wagner, “Challenges in autonomous vehicle testing and
validation,” SAE Int. J. Transp. Saf., vol. 4, no. 1, pp. 15–24,
2016, SAE World Congr. Exhib.

[ISO/PAS 21448:2022, 2022]
ISO/PAS 21448:2022, “Road vehicles – safety of the intended
functionality,” ISO, Tech. Rep., Jun. 2022.

[ISO 26262:2018, 2018]
ISO 26262:2018, “Road vehicles – functional safety,” ISO, Tech. Rep.,
Dec. 2018.

[Denney et al., 2012]
E. Denney, G. Pai, and J. Pohl, “Heterogeneous aviation safety cases:
Integrating the formal and the non-formal,” in IEEE 17th Int. Conf.
Eng. Complex Comput. Syst., 2012, pp. 199–208.

[Loos et al., 2011]
S. M. Loos, A. Platzer, and L. Nistor, “Adaptive cruise control: Hybrid,
distributed, and now formally verified,” in FM 2011: Formal Methods,
ser. LNCS, 2011, pp. 42–56.

[Nilsson et al., 2012]
P. Nilsson, N. Özay, U. Topcu, and R. M. Murray, “Temporal logic control
of switched affine systems with an application in fuel balancing,” in
Am. Control Conf., Jun. 2012, pp. 5302–5309.

[Wongpiromsarn et al., 2013]
T. Wongpiromsarn, U. Topcu, and R. M. Murray, “Synthesis of control protocols
for autonomous systems,” Unmanned Syst., vol. 01, no. 01, pp. 21–39,

[Korssen et al., 2018]
T. Korssen, V. Dolk, J. Van De Mortel-Fronczak, M. Reniers, and M. Heemels,
“Systematic model-based design and implementation of supervisors for
advanced driver assistance systems,” IEEE Trans. Intell. Transp.
Syst., vol. 19, no. 2, pp. 533–544, Feb. 2018.

[Selvaraj et al., 2022]
Y. Selvaraj, W. Ahrendt, and M. Fabian, “Formal development of safe automated
driving using differential dynamic logic,” IEEE Trans. Intell.
Veh., pp. 1–12, 2022.

[Krook et al., 2019]
J. Krook, L. Svensson, Y. Li, L. Feng, and M. Fabian, “Design and formal
verification of a safe stop supervisor for an automated vehicle,” in
Int. Conf. Robot. Autom., May 2019, pp. 5607–5613.

[Galloway et al., 2008]
A. Galloway, F. Iwu, J. McDermid, and I. Toyn, “On the formal development of
safety-critical software,” in First IFIP Conf. Verif. Softw.:
Theories, Tools, Exp. 2005, ser. LNCS, vol. 4171, 2008, pp. 362–373.

[Rushby, 2010]
J. Rushby, “Formalism in safety cases,” in Mak. Syst. Safer, ser.
SCSC, 2010, pp. 3–17, saf.-Crit. Syst. Symp.

[Habli and Kelly, 2009]
I. Habli and T. Kelly, “A generic goal-based certification argument for the
justification of formal analysis,” Electron. Notes Theor. Comput.
Sci., vol. 238, no. 4, pp. 27–39, Sep. 2009, first Workshop Certif.
Saf.-Crit. Softw. Control. Syst. (SafeCert 2008).

[Ministry of Defence, 2017]
Ministry of Defence, “Defence standard 00-56 part 1: Safety management
requirements for defence systems,” Tech. Rep., Feb. 2017.

[Kelly and Weaver, 2004]
T. Kelly and R. Weaver, “The goal structuring notation – a safety argument
notation,” in Int. Conf. Depend. Syst. Netw., Jul. 2004, workshop
Assur. Cases.

[ACWG, 2021]
ACWG, “Goal structuring notation community standard,” url:
<https://scsc.uk/r141C:1>, SCSC, Tech. Rep., May 2021.

[NASA, 2016]
NASA, “What is formal methods?” url:
<https://shemesh.larc.nasa.gov/fm/fm-what.html> (accessed 2022-07-26),
Apr. 2016.

[Baier and Katoen, 2008]
C. Baier and J.-P. Katoen, Principles of Model Checking.1em plus
0.5em minus 0.4emMIT Press, 2008.

[Platzer, 2018]
A. Platzer, Logical Foundations of Cyber-Physical Systems.1em
plus 0.5em minus 0.4emSpringer, 2018.

[Bergenhem et al., 2015]
C. Bergenhem, R. Johansson, A. Söderberg, J. Nilsson, J. Tryggvesson,
M. Törngren, and S. Ursing, “How to reach complete safety requirement
refinement for autonomous vehicles,” in Crit. Automot. Appl.: Robust.
Saf., Sep. 2015.

[Sangiovanni-Vincentelli et al., 2012]
A. Sangiovanni-Vincentelli, W. Damm, and R. Passerone, “Taming Dr.
Frankenstein: contract-based design for cyber-physical systems,”
Eur. J. Control, vol. 18, no. 3, pp. 217–238, 2012.

[Rodrigues de Campos et al., 2021]
G. Rodrigues de Campos, R. Kianfar, and M. Brännström, “Precautionary
safety for autonomous driving systems: Adapting driving policies to satisfy
quantitative risk norms,” in IEEE Intell. Transp. Syst. Conf.,
2021, pp. 645–652.

[Warg et al., 2020]
F. Warg, M. Skoglund, A. Thorsén, R. Johansson, M. Brännström,
M. Gyllenhammar, and M. Sanfridson, “The quantitative risk norm - a proposed
tailoring of HARA for ADS,” in 50th Annual IEEE/IFIP Int. Conf.
Depend. Syst. Netw. Workshops, 2020, pp. 86–93.

[Peden et al., 2004]
M. Peden, R. Scurfield, D. Sleet, D. Mohan, A. A. Hyder, E. Jarawan, and
C. Mathers, World report on road traffic injury prevention.1em
plus 0.5em minus 0.4emWorld Health Organization, Feb. 2004.

[Kwiatkowska et al., 2022]
M. Kwiatkowska, G. Norman, and D. Parker, “Probabilistic model checking and
autonomy,” Annual Rev. Control, Robot. Auton. Syst., vol. 5, pp.
385–410, 2022.

§ DISCUSSION POINTS

Probabilistic modelling Why don't we use probabilistic modelling and associated formal tools to argue ? Maybe we can include a discussion on how could be formalized in PCTL for instance and talk about how notoriously hard it is to model the system with the required probabilities, if at all possible. Will such a requirement be formalized like so?

\begin{equation*}
\pctl{\le 0.01}(\Diamond\,\phi)
\end{equation*}

Some potential questions that may come up (maybe some of them are not relevant but thinking out loud anyway):

* In our argument, we assume that and fulfill their respective formal assumptions with the indicated probability. Is that a reasonable assumption to make? Not saying that we should argue about the numbers but we should discuss how one might approach the problem that those components can indeed be verified to show that they are fulfilled.

* We also claim that formal methods helps to reduce the overall verification effort. It is sort of self explanatory through the GSN that we do not have to do as much closed-loop complete vehicle testing with our approach. But I think we should also talk about if there could be any threats to that claim? Could there be cases where our approach does not help at all? Could there be cases where testing the requirements on the individual components is as hard as complete vehicle testing?

* We should discuss about the role of machine learning in the design and development of ADS. Can our approach be adopted even if the components involve ML based algorithms?

* Is there a systematic way to do breakdown requirements without formally modelling all the respective components?

We should discuss:

* how the artifacts presented in  <ref> provide evidence to the GSN

* about the tool qualifications

* how this is only a part of the whole picture

* even if we manage to prove the specification, question the validity of the models (But the good thing is that we can use the formal models as a formal reference when validating.)

* draw parallels to contract based design. The consecutive pairs in the chain of models form assume-guarantee contracts.

* the contracts can be turned into runtime monitors.

* validating the formalization. Is the formalization more or less difficult than natural language breakdown?

* It might be useful to refer to <https://doi.org/10.1145/3372020.3391557>. It talks about “synthesizing” the assumptions from the guarantees. That way it could be possible to expand the ODD.

* how to actually show that the broken down goals imply the parent

What do we gain by this approach?

* We find problems on a high level without the need to implement anything.

* We get both a safe system, and a proof thereof.

* No need to review or test that the high level requirement is implied by the conjunction of the broken down requirements.

* If we know the speed we want to travel with, then we know what is required of the system and how to do it, not just evaluating and see what we get.

* Certification is made easier; the proof needs to be checked, but not the argument.

* Formalization removes ambiguity.

* Changes in can be formalized and verified. The breakdown only must be redone if the verification fails.

§ TITLE CANDIDATES

Keywords: Formal methods, Automated Driving, Evidence, Safety case, (Concept phase), Design phase

* Formal methods as evidence in automated vehicle safety case

* Supporting automated vehicle safety case with formal methods

* Using formal methods based evidence in automated driving safety case

* Formal methods as basis for evidence in automated driving safety case

* Using formal methods in an automated driving safety case

* Evidence arguments for using formal methods in automated driving safety case

* Arguments for using formal methods' evidence in automated driving safety case

* Formal methods supporting safety case

* Formal methods-supported safety case for automated driving systems

* Automated Driving Safety case: Formal methods approach

* Automated Driving Safety case: Providing evidence through formal methods

* A Formal Methods approach to provide evidence in automated driving safety cases

* Providing evidence in automated driving safety case through Formal Methods

* Automated Driving Safety Case: leveraging formal methods in the design phase

§ WHERE TO PARTAYYY!!

IEEE Journals

* <https://ieee-itss.org/pub/t-iv/> - TIV - short paper or practioner paper - 6 pages.

* <https://ieee-itss.org/pub/its-magazine/> - Regular paper is 8 pages. Suitable?

* <https://ieeesystemsjournal.org/> - Regular paper is max 12 pages but first 8 pages are complimentary. So might pass for just 8 pages long

* <https://www.ieee-ras.org/publications/ram/special-issues/special-issue-on-autonomous-vehicle-artificial-intelligence-and-model-based-techniques-in-decision-and-control> - Is this still open? Doubtful

* <https://www.ieee-ras.org/publications/ram/information-for-authors-ram#preparingmanuscript> - RA Magazine - 9 pages.

* <https://www.ieee-ras.org/publications/ra-l/information-for-authors-ra-l>

* <https://publication-recommender.ieee.org/pubsearch#> - Publication search

* <https://rs.ieee.org/publications/transactions-on-reliability.html> - This seems to be a pain.

* <https://conf.researchr.org/home/nfm-2023> NASA Formal methods, among other things, accepts research on formal methods for safety cases.

* <https://ieeesystemscouncil.org/document/syscon-2023-call-papers>

* <https://www.sae.org/attend/wcx/call-for-papers/connectivity-iot-smart-city>

* <http://www.icara.us/submission.html>

* <https://www.sae.org/publications/journals/calls-for-papers-transportation-safety>

* <https://jsystemsafety.com/>

§ HYPOTHESIS

The following is adapted from Licentiate thesis: We believe formal methods, and especially formal synthesis, can be applied in automotive development processes to generate useful and meaningful correct-by-construction tactical planners. Such formal methods should be beneficial because they alleviate drawbacks of other methods that cannot provide correctness proofs, specifically the processes of reviews and testing.

However, it is not well investigated how formal methods reasoning about closed-loop models are integrated with the safety case. The proven controller must be synchronized with the actual code, the specification must be correctly formalized and broken down from natural language requirements, and the assumptions on the vehicle model and the environment must go somewhere.

By showing how the artifacts mentioned above can support the safety case, we believe that formal methods may get a better reputation in system safety contexts and in the automotive industry at large.

§ RESEARCH QUESTIONS

RQ 1 How does the specification give support for the fulfillment of the safety goal?

RQ 2 How does the verified or synthesized controller model support the correctness argument of the implementation?

RQ 3 How is environment assumptions relating to system features pushed to other parts of the safety case?

RQ 4 How is environment assumptions relating to the external environment pushed to the ODD definition?

Also some (modified) research gaps from Magnus' work that may be worth considering:

* How do we show that ODD, model assumptions, and real world uncertainties cover the same behaviors in enough degree?

* How do we show that the controller takes care of all the hazards, given that the controller affects exposure, and thereby may exclude hazards? And how do we list “all” hazards then?

* How do we handle requirements that cannot be formalized? (For us it is probably rather a question on how to interpret the assumptions on the perception system.) [id=YS]We must be careful about dealing with this question. There is a risk that we might not be able to convey the message without presenting detailed information about perception system. Probably best to draw the boundary before we start addressing this.

* Is there a way to frame formal methods as a way to automate parts of HARA?

* How do we combine the quantitative requirements from PCS with the qualitative requirements in formal methods?

* Do these methods have problems with scaling to automotive applications? If so, are there ways to overcome them? [id=YS]Could automation be considered as a tool to aid scaling? If so, could we combine the research gap about automating HARA with this one? Scaling could mean many things: 1. How do we address more use cases — here the challenge is to tackle the curse of dimensionality. 2. How can we tackle the effort required to leverage formal methods in the development process? Both are interesting challenges to address. We tell the story based on how the preliminary results are obtained.

I think formal methods can chip away at these questions. Not that they answer the questions completely, but formal methods should address these questions in certain parts of the safety case.

§ RELATED WORK SUMMARIES

Denney et al., 2012 present an automatic method to assemble safety cases based on the output of formal software verification. They verify in open loop.

Habli and Kelly, 2009 Testing is a powerful method of verification. […] However, formal analytical techniques are now well established and proven and can replace testing for certain applications, at least for the verification of the software at the unit and software integration level. This paper presents a generic GSN argument that justifies the use of a formal methods tool of choice.

Galloway et al., 2008 Few software development models relate the software to the embedding system/environment; Abstractly, requirements for the control system are stated in terms of relationships over the monitored and controlled variables, whilst specifications for the computer system are stated in terms of input and output variables. This paper seems to be very relevant. They list challenges for introducing a formal methods based development for safety critical systems. They seem to argue in terms of some kind of abstract interpretation context that the environment should be taken into account when formally proving properties of software. They still talk about pre and post conditions though. They do not mention how the safety case should be argued.

Rushby, 2010 Argues that formal methods should provide benefits everywhere in the safety case. The high-level arguments can be checked for soundness with deductive verification. Lower-level arguments can be verified by a multitude of formal verification tools. Probability is mentioned in conjunction with formalization, but only where formalization can prove correctness and eliminate the need of analysing failure probabilities. It is also argued that formal methods can be of great help to put focus on evidence and assumptions (validation) instead of verification of the soundness of the safety case. The sentiment put forward is much in line with what is put forward in this paper, but it lacks the specifics.

* <cit.> Uses simulink design verifier to model check a simulink model that is on par with an industrial example. They discuss how model checking might be used in safety assurance. They only care about input/output systems. They conclude that formal methods in assurance cases might be unjustified because of the overhead costs, but it seems like they overestimates its importance. The overhead costs should not be incurred at all times that a traditional review is performed; however, this is what they seem to compare to.

Korssen et al., 2018

* <cit.>

Wongpiromsarn et al., 2013

Loos et al., 2011

* Reference [3] – [9] from PCS paper can also be used to some extent, but I do not propose to use them all. Might be good to use RSS and something from Althoff, maybe that is enough in addition to what is already listed. RSS and Althoff do not use formal methods as we define them, but might be good to mention them and state that they do not provide an argument for how to argue in the safety case.

[SAE J3016`_202104, 2021]
SAE J3016`_202104, “Taxonomy and definitions for terms related to
driving automation systems for on-road motor vehicles,” SAE Int., Tech.
Rep., Apr. 2021.

[EU:, 2019]
“Regulation (EU) 2019/2144 of the European Parliament,” url:
<http://data.europa.eu/eli/reg/2019/2144/oj>, Dec. 2019.

[Eugensson et al., 2013]
A. Eugensson, M. Brännström, D. Frasher, M. Rothoff, S. Solyom, and
A. Robertsson, “Environmental, safety, legal and societal implications of
autonomous driving systems,” in Int. Tech. Conf. Enhanc. Saf. Veh.,
vol. 334, 2013.

[Lubbe et al., 2018]
N. Lubbe, H. Jeppsson, A. Ranjbar, J. Fredriksson, J. Bärgman, and
M. Östling, “Predicted road traffic fatalities in germany: The potential
and limitations of vehicle safety technologies from passive safety to highly
automated driving,” in Int. Res. Counc. Biomech. Inj., Sep. 2018, pp.

[Kalra and Paddock, 2016]
N. Kalra and S. M. Paddock, Driving to Safety: How Many Miles of Driving
Would It Take to Demonstrate Autonomous Vehicle Reliability?1em plus
0.5em minus 0.4emRAND Corporation, 2016.

[Koopman and Wagner, 2017]
P. Koopman and M. Wagner, “Autonomous vehicle safety: An interdisciplinary
challenge,” IEEE Intell. Transp. Syst. Mag., vol. 9, no. 1, pp.
90–96, Jan. 2017.

[Koopman et al., 2019]
P. Koopman, A. Kane, and J. Black, “Credible autonomy safety argumentation,”
in 27th Saf.-Crit. Syst. Symp., Feb. 2019.

[Koopman and Wagner, 2016]
P. Koopman and M. Wagner, “Challenges in autonomous vehicle testing and
validation,” SAE Int. J. Transp. Saf., vol. 4, no. 1, pp. 15–24,
2016, SAE World Congr. Exhib.

[ISO/PAS 21448:2022, 2022]
ISO/PAS 21448:2022, “Road vehicles – safety of the intended
functionality,” ISO, Tech. Rep., Jun. 2022.

[ISO 26262:2018, 2018]
ISO 26262:2018, “Road vehicles – functional safety,” ISO, Tech. Rep.,
Dec. 2018.

[Denney et al., 2012]
E. Denney, G. Pai, and J. Pohl, “Heterogeneous aviation safety cases:
Integrating the formal and the non-formal,” in IEEE 17th Int. Conf.
Eng. Complex Comput. Syst., 2012, pp. 199–208.

[Loos et al., 2011]
S. M. Loos, A. Platzer, and L. Nistor, “Adaptive cruise control: Hybrid,
distributed, and now formally verified,” in FM 2011: Formal Methods,
ser. LNCS, 2011, pp. 42–56.

[Nilsson et al., 2012]
P. Nilsson, N. Özay, U. Topcu, and R. M. Murray, “Temporal logic control
of switched affine systems with an application in fuel balancing,” in
Am. Control Conf., Jun. 2012, pp. 5302–5309.

[Wongpiromsarn et al., 2013]
T. Wongpiromsarn, U. Topcu, and R. M. Murray, “Synthesis of control protocols
for autonomous systems,” Unmanned Syst., vol. 01, no. 01, pp. 21–39,

[Korssen et al., 2018]
T. Korssen, V. Dolk, J. Van De Mortel-Fronczak, M. Reniers, and M. Heemels,
“Systematic model-based design and implementation of supervisors for
advanced driver assistance systems,” IEEE Trans. Intell. Transp.
Syst., vol. 19, no. 2, pp. 533–544, Feb. 2018.

[Selvaraj et al., 2022]
Y. Selvaraj, W. Ahrendt, and M. Fabian, “Formal development of safe automated
driving using differential dynamic logic,” IEEE Trans. Intell.
Veh., pp. 1–12, 2022.

[Krook et al., 2019]
J. Krook, L. Svensson, Y. Li, L. Feng, and M. Fabian, “Design and formal
verification of a safe stop supervisor for an automated vehicle,” in
Int. Conf. Robot. Autom., May 2019, pp. 5607–5613.

[Galloway et al., 2008]
A. Galloway, F. Iwu, J. McDermid, and I. Toyn, “On the formal development of
safety-critical software,” in First IFIP Conf. Verif. Softw.:
Theories, Tools, Exp. 2005, ser. LNCS, vol. 4171, 2008, pp. 362–373.

[Rushby, 2010]
J. Rushby, “Formalism in safety cases,” in Mak. Syst. Safer, ser.
SCSC, 2010, pp. 3–17, saf.-Crit. Syst. Symp.

[Habli and Kelly, 2009]
I. Habli and T. Kelly, “A generic goal-based certification argument for the
justification of formal analysis,” Electron. Notes Theor. Comput.
Sci., vol. 238, no. 4, pp. 27–39, Sep. 2009, first Workshop Certif.
Saf.-Crit. Softw. Control. Syst. (SafeCert 2008).

[Ministry of Defence, 2017]
Ministry of Defence, “Defence standard 00-56 part 1: Safety management
requirements for defence systems,” Tech. Rep., Feb. 2017.

[Kelly and Weaver, 2004]
T. Kelly and R. Weaver, “The goal structuring notation – a safety argument
notation,” in Int. Conf. Depend. Syst. Netw., Jul. 2004, workshop
Assur. Cases.

[ACWG, 2021]
ACWG, “Goal structuring notation community standard,” url:
<https://scsc.uk/r141C:1>, SCSC, Tech. Rep., May 2021.

[NASA, 2016]
NASA, “What is formal methods?” url:
<https://shemesh.larc.nasa.gov/fm/fm-what.html> (accessed 2022-07-26),
Apr. 2016.

[Baier and Katoen, 2008]
C. Baier and J.-P. Katoen, Principles of Model Checking.1em plus
0.5em minus 0.4emMIT Press, 2008.

[Platzer, 2018]
A. Platzer, Logical Foundations of Cyber-Physical Systems.1em
plus 0.5em minus 0.4emSpringer, 2018.

[Bergenhem et al., 2015]
C. Bergenhem, R. Johansson, A. Söderberg, J. Nilsson, J. Tryggvesson,
M. Törngren, and S. Ursing, “How to reach complete safety requirement
refinement for autonomous vehicles,” in Crit. Automot. Appl.: Robust.
Saf., Sep. 2015.

[Sangiovanni-Vincentelli et al., 2012]
A. Sangiovanni-Vincentelli, W. Damm, and R. Passerone, “Taming Dr.
Frankenstein: contract-based design for cyber-physical systems,”
Eur. J. Control, vol. 18, no. 3, pp. 217–238, 2012.

[Rodrigues de Campos et al., 2021]
G. Rodrigues de Campos, R. Kianfar, and M. Brännström, “Precautionary
safety for autonomous driving systems: Adapting driving policies to satisfy
quantitative risk norms,” in IEEE Intell. Transp. Syst. Conf.,
2021, pp. 645–652.

[Warg et al., 2020]
F. Warg, M. Skoglund, A. Thorsén, R. Johansson, M. Brännström,
M. Gyllenhammar, and M. Sanfridson, “The quantitative risk norm - a proposed
tailoring of HARA for ADS,” in 50th Annual IEEE/IFIP Int. Conf.
Depend. Syst. Netw. Workshops, 2020, pp. 86–93.

[Peden et al., 2004]
M. Peden, R. Scurfield, D. Sleet, D. Mohan, A. A. Hyder, E. Jarawan, and
C. Mathers, World report on road traffic injury prevention.1em
plus 0.5em minus 0.4emWorld Health Organization, Feb. 2004.

[Kwiatkowska et al., 2022]
M. Kwiatkowska, G. Norman, and D. Parker, “Probabilistic model checking and
autonomy,” Annual Rev. Control, Robot. Auton. Syst., vol. 5, pp.
385–410, 2022.


[]Maximilian Hauck []Maximilian Hauck

#  $d$-th roots of determinants of generators of $\mathcal{C}_{6}$-subgroups
of $\GL(d,q)$ in $\mathbb{F}_{q}$

Maximilian Hauck

##  1 Introduction

The maximal subgroups of the finite classical groups can be partitioned into
nine classes according to Aschbacher’s theorem [A84]. We are concerned here
with the class $\mathcal{C}_{6}$ consisting of normalisers of extraspecial
groups or of two-groups of symplectic type. In [HR05], explicit constructions
are given for generators of these subgroups. Namely, for
$\operatorname{SL}(d,q)$, this is done by first describing generators of the
respective normalisers in $\operatorname{GL}(d,q)$ and afterwards
appropriately scaling them so that they lie in $\operatorname{SL}(d,q)$.
Effectively, this comes down to finding a $d$-th root of the determinants of
the generators in $\mathbb{F}_{q}$.

In [HR05]*Proposition 9.5, it is claimed that this can be done in almost all
cases with only a few exceptions, but no detailed explanation or analysis is
given why this is true or when exactly this is possible. This paper works out
the missing details by examining the relevant determinants and giving a
complete description of the cases in which they are $d$-th powers in
$\mathbb{F}_{q}$. Furthermore, it turns out that these determinants are
actually already $1$ in many cases so that one can omit the scaling entirely –
particularly for large $q$, this may save some time in practical computations.

##  2 Results

Let $q=p^{e}$ be a prime power and $r$ a prime dividing $q-1$. Let $d=r^{m}$
and $\omega$ be a primitive $r$-th root of unity in $\mathbb{F}_{q}$. We
define the following matrices:

  1. 1.

Let $U\in\operatorname{GL}(r,q)$ be diagonal with
$U_{ii}=\omega^{\frac{i(i-1)}{2}}$ for $1\leq i\leq r$.

  2. 2.

Let $V\in\operatorname{GL}(r,q)$ with $V_{ij}=\omega^{(i-1)(j-1)}$ for $1\leq
i,j\leq r$.

  3. 3.

For $m\geq 2$, let $W\in\operatorname{GL}(r^{2},q)$ be the permutation matrix
defined by the permutation $w\in\operatorname{Sym}(\\{0,\dots,r^{2}-1\\})$
given by $a\mapsto(a+((a-1)\mod r)\cdot r)\mod r^{2}$.

  4. 4.

$U_{i}:=I_{r^{m-i}}\otimes U\otimes I_{r^{i-1}}$ for $1\leq i\leq m$.

  5. 5.

$V_{i}:=I_{r^{m-i}}\otimes V\otimes I_{r^{i-1}}$ for $1\leq i\leq m$.

  6. 6.

$W_{i}:=I_{r^{m-1-i}}\otimes W\otimes I_{r^{i-1}}$ for $1\leq i\leq m$.

Notice that our definition of the Kronecker product is the same as in [HR05].
Most importantly, for an $n\times n$-matrix $A$ and an $m\times m$-matrix $B$,
it holds that $\det(A\otimes B)=\det(A)^{m}\det(B)^{n}$.

We will prove the following:

######  Theorem 1.

The determinant of $U_{i}$ has a $d$-th root in $\mathbb{F}_{q}$ except when
$r\leq 3$ and $m=1$ and $r^{2}\nmid q-1$. Moreover if $r>3$ or $m\geq 2$, we
have $\det U_{i}=1$.

######  Theorem 2.

The determinant of $V_{i}$ has a $d$-th root in $\mathbb{F}_{q}$ except when
$r=2$, $e$ is odd, and either $m=2$ and $p\equiv 1,3,7\pmod{8}$, or $m=1$ and
$p\equiv 1,3\pmod{8}$.

######  Theorem 3.

For $m\geq 2$, the determinant of $W_{i}$ has a $d$-th root in
$\mathbb{F}_{q}$ except when $r=2$ and $m=2$ and $8\nmid q-1$. Moreover if
$r>2$ or $m\geq 3$, we have $\det W_{i}=1$.

##  3 Proofs

######  Lemma 4.

If $r>3$, then $\det U=1$. Otherwise, $r=2$ or $r=3$ and $\det U=\omega$.

###### Proof.

We have

$\sum_{i=1}^{r}\frac{i(i-1)}{2}=\frac{1}{2}\sum_{i=1}^{r}i^{2}-\frac{1}{2}\sum_{i=1}^{r}i=\frac{1}{2}\cdot\frac{r(r+1)(2r+1)}{6}-\frac{1}{2}\cdot\frac{r(r+1)}{2}=\frac{(r-1)r(r+1)}{6},$

and therefore

$\det
U=\prod_{i=1}^{r}\omega^{\frac{i(i-1)}{2}}=\omega^{\frac{(r-1)r(r+1)}{6}}.$

For $r=2$ or $r=3$ this yields $\det U=\omega$. For $r>3$, since $r$ is a
prime, either $r-1$ or $r+1$ is divisible by $3$ and both are even. Hence
$\ell:=\frac{(r-1)(r+1)}{6}$ is an integer and $\det U=\omega^{r\ell}=1$. ∎

######  Proposition 5.

If $r>3$ or $m\geq 2$, we have $\det U_{i}=1$. Otherwise, $r\leq 3$ and $m=1$
and $\det V_{i}$ admits a $d$-th root in $\mathbb{F}_{q}$ if and only if
$r^{2}\mid q-1$.

###### Proof.

Firstly,

$\det U_{i}=\det\left(\left(I_{r^{m-i}}\otimes U\right)\otimes
I_{r^{i-1}}\right)=\det\left(I_{r^{m-i}}\otimes U\right)^{r^{i-1}}=\left((\det
U)^{r^{m-i}}\right)^{r^{i-1}}=(\det U)^{r^{m-1}}.$

Using 4, we immediately get $\det U_{i}=1$ in the case $r>3$. So consider
$r\leq 3$; if $m\geq 2$, using 4 we obtain

$\det U_{i}=\omega^{r^{m-1}}=1$

since $\omega$ is an $r$-th root of unity. Finally, if $r\leq 3$ and $m=1$, we
get $\det U_{i}=\omega$. In this case, since $\omega$ is a primitive $r$-th
root of unity, we can find a $d$-th root (i.e. $r$-th root) of $\det
U_{i}=\omega$ in $\mathbb{F}_{q}$ if and only if there exist primitive
$r^{2}$-th roots of unity in $\mathbb{F}_{q}$, i.e. if and only if $r^{2}\mid
q-1$. ∎

5 immediately implies Theorem 1.

######  Lemma 6.

We have $\det V=\omega-1$ if $r=2$ and $\det V=3\omega(\omega-1)$ if $r=3$. If
$r>3$, we have

$\det V=\prod_{k=1}^{r-1}(\omega^{k}-1)^{r-k}.$

###### Proof.

Since $V$ is a Vandermonde-type matrix, we have

$\begin{split}\det V&=\prod_{0\leq i<j\leq
r-1}(\omega^{j}-\omega^{i})=\prod_{i=0}^{r-2}\prod_{j=i+1}^{r-1}\omega^{i}(\omega^{j-i}-1)=\prod_{i=0}^{r-2}\prod_{k=1}^{r-1-i}\omega^{i}(\omega^{k}-1)\\\
&=\prod_{i=0}^{r-2}\omega^{i(r-1-i)}\prod_{k=1}^{r-1-i}(\omega^{k}-1)=\omega^{\sum_{i=0}^{r-2}i(r-1-i)}\prod_{i=0}^{r-2}\prod_{k=1}^{r-1-i}(\omega^{k}-1)\\\
&=\omega^{\sum_{i=0}^{r-2}i(r-1-i)}\prod_{k=1}^{r-1}\prod_{i=0}^{r-1-k}(\omega^{k}-1)=\omega^{\sum_{i=0}^{r-2}i(r-1-i)}\prod_{k=1}^{r-1}(\omega^{k}-1)^{r-k}.\end{split}$

Furthermore,

$\begin{split}\sum_{i=0}^{r-2}i(r-1-i)&=\sum_{i=1}^{r-1}i(r-1-i)=(r-1)\sum_{i=1}^{r-1}i-\sum_{i=1}^{r-1}i^{2}\\\
&=(r-1)\cdot\frac{r(r-1)}{2}-\frac{r(r-1)(2r-1)}{6}=\frac{(r-2)(r-1)r}{6}.\end{split}$

Evaluating these expressions for the cases $r=2$ and $r=3$ is easy and gives
$\det V=\omega-1$ and $\det V=3\omega(\omega-1)$, respectively, as claimed.

Now let $r>3$. Then $r-1$ is even and one of $r-2$ and $r-1$ is divisible by
$3$, i.e. $\frac{(r-2)(r-1)}{6}=:\ell\in\mathbb{N}$, which means

$\det
V=\omega^{r\ell}\prod_{k=1}^{r-1}(\omega^{k}-1)^{r-k}=\prod_{k=1}^{r-1}(\omega^{k}-1)^{r-k}.\qed$

######  Lemma 7.

If $r\geq 3$, then $\det V$ admits an $r$-th root in $\mathbb{F}_{q}$.

###### Proof.

The case $r=3$ is easy because, using 6,

$(1-\omega)^{3}=1-3\omega+3\omega^{2}-\omega^{3}=3\omega(\omega-1)=\det V.$

Now consider $r\geq 3$. On the one hand, 6 shows that

$\det V=\prod_{k=1}^{r-1}(\omega^{k}-1)^{r-k}.$ (1)

On the other hand, using $\omega^{r}=1$, we can also write this as

$\det
V=\prod_{k=1}^{r-1}(\omega^{k}-\omega^{r})^{r-k}=\prod_{k=1}^{r-1}\omega^{k(r-k)}(1-\omega^{r-k})^{r-k}=\omega^{\sum_{k=1}^{r-1}k(r-k)}\prod_{k=1}^{r-1}(1-\omega^{r-k})^{r-k}.$

Computing $\sum_{k=1}^{r-1}k(r-k)$ is similar to the computation of the sum
occurring in the proof of 6 and gives $\frac{(r-1)r(r+1)}{6}$. Again, as
$r>3$, one of $r-1$ and $r+1$ must be divisible by $3$ and $r-1$ is even – so
$\frac{(r-1)r(r+1)}{6}=:\ell\in\mathbb{N}$ and

$\det
V=\omega^{r\ell}\prod_{k=1}^{r-1}(1-\omega^{r-k})^{r-k}=\prod_{k=1}^{r-1}(1-\omega^{r-k})^{r-k}=\prod_{k=1}^{r-1}(1-\omega^{k})^{k}.$

Recall the definition of the Legendre symbol and note that the number of odd
integers between $1$ and $r-1$ is even if and only if $r-1$ is divisible by
$4$, i.e., by quadratic reciprocity, if and only if $-1$ is a quadratic
residue mod $r$ (remember that $r$ is odd). Therefore

$\det V=\left(\frac{-1}{r}\right)\prod_{k=1}^{r-1}(\omega^{k}-1)^{k}.$ (2)

Instead of further simplifying $\det V$ directly, we can obtain an expression
for $(\det V)^{2}$ by multiplying equations (1) and (2):

$(\det
V)^{2}=\left(\frac{-1}{r}\right)\prod_{k=1}^{r-1}(\omega^{k}-1)^{r}=\left(\frac{-1}{r}\right)\left(\prod_{k=1}^{r-1}(\omega^{k}-1)\right)^{r}$

Now observe that since $2$ and $r$ are coprime, $\det V$ is an $r$-th power in
$\mathbb{F}_{q}$ if and only if $(\det V)^{2}$ is an $r$-th power. However,
for $(\det V)^{2}$, this is obvious: The second factor is clearly an $r$-th
power and the first one is, too: Indeed, again since $2$ and $r$ are coprime,
$\left(\frac{-1}{r}\right)$ is an $r$-th power if and only if
$\left(\frac{-1}{r}\right)^{2}=1$ is an $r$-th power – but this is trivial. In
conclusion, $\det V$ is an $r$-th power and by our remark above we can thus
find a $d$-th root of $\det V_{i}$ in $\mathbb{F}_{q}$. ∎

######  Remark 8.

If $r>3$, using the expression for $(\det V)^{2}$ from the previous proof, we
can make some further simplifications and obtain

$(\det V)^{2}=\left(\frac{-1}{r}\right)r^{r}.$

######  Proposition 9.

If $r\geq 3$, then $\det V_{i}$ admits a $d$-th root in $\mathbb{F}_{q}$.

###### Proof.

As in the proof of 5,

$\det V_{i}=(\det V)^{r^{m-1}}.$

However, by 7, we can find an $r$-th root of $\det V$ in $\mathbb{F}_{q}$ and
thereby a $d$-th root of $\det V_{i}$ in $\mathbb{F}_{q}$ (recall $d=r^{m}$).
∎

Recall $q=p^{e}$ where $p$ is prime.

######  Proposition 10.

If $r=2$ and $m\geq 3$, then $\det V_{i}$ admits a $d$-th root in
$\mathbb{F}_{q}$. Otherwise, $r=2$ and $m\leq 2$ and $\det V_{i}$ admits a
$d$-th root in $\mathbb{F}_{q}$ if and only if one of the following holds:

  1. (i)

$e$ is even,

  2. (ii)

$p\equiv 1,3\pmod{8}$ or

  3. (iii)

$p\equiv 7\pmod{8}$ and $m=2$.

###### Proof.

As in the proof of 5,

$\det V_{i}=(\det V)^{2^{m-1}}.$

Now note that as $\omega$ is a primitive $r$-th root of unity and $r=2$, we
have $\omega=-1$. Using 6, this gives $\det V=\omega-1=-2$. We begin with
$m\geq 3$ and consider three cases:

  1. I.

$p\equiv 1,3\pmod{8}$. By quadratic reciprocity, $-2$ is a square mod $p$;
hence $\det V=-2$ is a square in $\mathbb{F}_{q}$ and thus we can find a
$d$-th root of $\det V_{i}=(\det V)^{2^{m-1}}$ in $\mathbb{F}_{q}$ (recall
$d=r^{m}=2^{m}$). Note that this argument works for all values of $m$.

  2. II.

$p\equiv 7\pmod{8}$. By quadratic reciprocity, $2$ is a square mod $p$; hence
$(\det V)^{2}=4=2^{2}$ is a fourth power in $\mathbb{F}_{q}$. Since $m\geq 2$,
we can write

$\det V_{i}=(\det V)^{2^{m-1}}=\left((\det V)^{2}\right)^{2^{m-2}}$

and as $(\det V)^{2}$ is a fourth power, we can find a $d$-th root of $\det
V_{i}$ in $\mathbb{F}_{q}$. Note that this argument only requires $m\geq 2$.

  3. III.

$p\equiv 5\pmod{8}$. By quadratic reciprocity, $-1$ is a square mod $p$ and
hence we can find $i\in\mathbb{F}_{p}$ with $i^{2}=-1$. Note that, again by
quadratic reciprocity, $2$ is a quadratic non-residue mod $p$ and so, by
Euler’s criterion,

$(2i)^{\frac{p-1}{2}}=2^{\frac{p-1}{2}}i^{\frac{p-1}{2}}=\left(\frac{2}{p}\right)\cdot(-1)=1.$

Thus, applying Euler’s criterion the other way around (i.e. to
$2i\in\mathbb{F}_{p}$), $2i$ is a square mod $p$. Hence, $(\det
V)^{4}=16=(2i)^{4}$ is an eighth power in $\mathbb{F}_{q}$. Since $m\geq 3$,
we can write

$\det V_{i}=(\det V)^{2^{m-1}}=\left((\det V)^{4}\right)^{2^{m-3}}$

and due to $(\det V)^{4}$ being an eighth power, we can find a $d$-th root of
$\det V_{i}$ in $\mathbb{F}_{q}$.

In conclusion, we can always find a $d$-th root of $\det V_{i}$ in
$\mathbb{F}_{q}$ for $r=2$ whenever $m\geq 3$, as claimed.

Now for the case $m\leq 2$, where we first show that the conditions (i)-(iii)
are sufficient. If (i) is true, i.e. $e$ is even, then we can find a square
root of $\det V=-2$ in the field $\mathbb{F}_{p^{2}}\leq\mathbb{F}_{q}$ and
therefore we can find a $d$-th root of $\det V_{i}=(\det V)^{2^{m-1}}$ in
$\mathbb{F}_{q}$. If (ii) is true, i.e. $p\equiv 1,3\pmod{8}$, we can use the
argument in I. to show that a $d$-th root of $\det V_{i}$ exists in
$\mathbb{F}_{q}$. If (iii) is true, i.e. $p\equiv 7\pmod{8}$ and $m=2$, we can
use the argument in II. to show that a $d$-th root of $\det V_{i}$ exists in
$\mathbb{F}_{q}$.

Finally, we show that in the case $m\leq 2$, at least one of the conditions
(i)-(iii) must hold for a $d$-th root of $\det V_{i}$ to exist in
$\mathbb{F}_{q}$. First consider the case $m=1$ and assume $\det V_{i}=\det
V=-2$ has a $d$-th root, i.e. a square root, in $\mathbb{F}_{q}$. If $-2$ has
a square root in $\mathbb{F}_{p}$, we get $p\equiv 1,3\pmod{8}$ by quadratic
reciprocity, i.e. condition (ii). If $-2$ does not have a square root in
$\mathbb{F}_{p}$, but has a square root in $\mathbb{F}_{q}$, then the
polynomial $X^{2}+2$ is irreducible over $\mathbb{F}_{p}$ and splits over
$\mathbb{F}_{q}$ – in other words, the splitting field of $X^{2}+2$ is a
quadratic extension of $\mathbb{F}_{p}$, i.e. $\mathbb{F}_{p^{2}}$, and it is
a subfield of $\mathbb{F}_{q}$; hence, $\mathbb{F}_{p^{2}}\leq\mathbb{F}_{q}$,
which means $2\mid e$ and this is condition (i). So we have shown that if
$m=1$ and $\det V_{i}$ has a $d$-th root in $\mathbb{F}_{q}$, then at least
one of (i) and (ii) must hold.

It remains to consider the case $m=2$. Again, assume that $\det V_{i}=(\det
V)^{2}=4$ has a $d$-th root, i.e. a fourth root, in $\mathbb{F}_{q}$. This
implies that either $2$ or $-2$ has a square root in $\mathbb{F}_{q}$. If the
latter is the case, then the preceding paragraph shows that at least one of
(i) and (ii) must hold, so assume the former, i.e. $2$ is a square in
$\mathbb{F}_{q}$. We use a similar reasoning to the preceding paragraph: If
$2$ is a square in $\mathbb{F}_{p}$, we get $p\equiv 1,7\pmod{8}$ by quadratic
reciprocity, i.e. condition (ii) or condition (iii). If $2$ is not a square in
$\mathbb{F}_{p}$, but is a square in $\mathbb{F}_{q}$, then the polynomial
$X^{2}-2$ is irreducible over $\mathbb{F}_{p}$ and splits over
$\mathbb{F}_{q}$ – in other words, the splitting field of $X^{2}-2$ is a
quadratic extension of $\mathbb{F}_{p}$, i.e. $\mathbb{F}_{p^{2}}$, and it is
a subfield of $\mathbb{F}_{q}$; hence, $\mathbb{F}_{p^{2}}\leq\mathbb{F}_{q}$,
which means $2\mid e$ and this is condition (i). So if $m=2$ and $\det V_{i}$
has a $d$-th root in $\mathbb{F}_{q}$, then we have demonstrated that at least
one of (i)-(iii) must hold.

In conclusion, in the case $m\leq 2$, if $\det V_{i}$ has a $d$-th root in
$\mathbb{F}_{q}$, then one of the conditions (i)-(iii) must hold, as claimed.
∎

9 and 10 readily imply Theorem 2.

######  Lemma 11.

If $r>2$, then $\det W=1$. Otherwise, $r=2$ and $\det W=-1$.

###### Proof.

The determinant of $W$ is the sign of the permutation $w$. We will show that
$w$ is a product of $r-1$ cycles of length $r$ from which the result follows.

To prove this, write $a=ur+v$ with $0\leq u,v\leq r-1$; obviously, this is
unique. If $v>0$, $a$ maps to

$((ur+v)+(v-1)r)\mod r^{2}=((u+v-1)r+v)\mod r^{2}=((u+(v-1))\mod r)\cdot r+v;$

if $v=0$ and $u>0$, $a$ maps to

$(ur+(r-1)r)\mod r^{2}=(u-1)r$

and finally, if $u=v=0$, $a$ maps to $r(r-1)$. Observe that the image always
has the same value of $v$ as the pre-image; thus, we will consider each value
of $v$ separately. For $v=0$, we have just the $r$-cycle
$(r(r-1),r(r-2),\dots,2r,r,0)$. Now consider $v>1$; then starting from $v$ and
iteratively applying the permutation $w$, we successively get

$\begin{split}((v-1)\mod r)\cdot r+v,\hskip 14.22636pt&(2(v-1)\mod r)\cdot
r+v,\\\ &(3(v-1)\mod r)\cdot r+v,\hskip 14.22636pt\dots.\end{split}$

However, since $r$ is prime, the multiples of $v-1$ will take any value mod
$r$ (recall $0<v-1<r$) and consequently, by iteratively applying the
permutation $w$, we can get to any $ur+v$ with $0\leq u\leq r-1$ starting from
$v$ – i.e., we get an $r$-cycle for any $v>1$. Finally, it is obvious that $w$
fixes all $a$ with $v=1$. Summarising the results, $w$ is a product of exactly
$r-1$ cycles of length $r$, as claimed. ∎

######  Proposition 12.

If $r>2$ or $m\geq 3$, we have $\det W_{i}=1$. Otherwise, $r=m=2$ and $\det
W_{i}$ admits a $d$-th root in $\mathbb{F}_{q}$ if and only if $8\mid q-1$.

###### Proof.

Similarly to the proof of 5,

$\det W_{i}=(\det W)^{r^{m-2}}.$

Using 11, this means $\det W_{i}=1$ if $r>2$. If $r=2$ and $m\geq 3$, we also
get $\det W_{i}=1$ from 11. Finally, in the remaining case $r=m=2$ 11 give
$\det W_{i}=-1$ and we can find a $d$-th root of $\det W_{i}$ if and only if
$-1$ is a fourth power in $\mathbb{F}_{q}$ (recall that $d=r^{m}$). This,
however, occurs if and only if there are primitive eighth roots of unity in
$\mathbb{F}_{q}$, i.e. if and only if $8\mid q-1$. ∎

12 yields Theorem 3.

## References