English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Tools annual

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Tools monthly

Global: Zendy Plus monthly

Presents the access of premium content as premium feature

Premium Content

Global: Zendy Plus annual

Global: Zendy Free Plan

If autonomous vehicles are to be widely accepted, we need to ensure theirsafe operation. For this reason, verification and validation (V&V) approachesmust be developed that are suitable for this domain. Model checking is a formaltechnique which allows us to exhaustively explore the paths of an abstractmodel of a system. Using a probabilistic model checker such as PRISM, we maydetermine properties such as the expected time for a mission, or theprobability that a specific mission failure occurs. However, model checking ofcomplex systems is difficult due to the loss of information during abstraction.This is especially so when considering systems such as autonomous vehicleswhich are subject to external influences. An alternative solution is the use ofMonte Carlo simulation to explore the results of a continuous-time model of thesystem. The main disadvantage of this approach is that the approach is notexhaustive as not all executions of the system are analysed. We are thereforeinterested in developing a framework for formal verification of autonomousvehicles, using Monte Carlo simulation to inform and validate our symbolicmodels during the initial stages of development. In this paper, we present acontinuous-time model of a quadrotor unmanned aircraft undertaking anautonomous mission. We employ this model in Monte Carlo simulation to obtainspecific mission properties which will inform the symbolic models employed informal verification.

A Continuous-Time Model of an Autonomous Aerial Vehicle to Inform and Validate Formal Verification Methods