About: Validating Multiple Variants of an Automotive Light System with Electrum

Facets (new session)
Description
Metadata
Settings
- owl:sameAs
- Inference Rule:

About: Validating Multiple Variants of an Automotive Light System with Electrum Goto Sponge NotDistinct Permalink

An Entity of Type : schema:ScholarlyArticle, within Data Space : covidontheweb.inria.fr associated with source document(s)

Attributes	Values
type	Academic Article research paper schema:ScholarlyArticle
isDefinedBy	Covid-on-the-Web dataset
has title	Validating Multiple Variants of an Automotive Light System with Electrum
Creator	Liu, Chong Cunha, Alcino Macedo, Nuno
Source	PMC
abstract	This paper reports on the development and validation of a formal model for an automotive adaptive exterior lights system (ELS) with multiple variants in Electrum, a lightweight formal specification language that extends Alloy with mutable relations and temporal logic. We explore different strategies to address variability, one in pure Electrum and another through an annotative language extension. We then show how Electrum and its Analyzer can be used to validate systems of this nature, namely by checking that the reference scenarios are admissible, and to automatically verify whether the established requirements hold. A prototype was developed to translate the provided validation sequences into Electrum and back to further automate the validation process. The resulting ELS model was validated against the provided validation sequences and verified for most of requirements for all variants.
has issue date	2020-04-22(xsd:dateTime)
bibo:doi	10.1007/978-3-030-48077-6_26
has license	no-cc
sha1sum (hex)	259a52b573e278d5279541c5b877c546057301f4
schema:url	https://doi.org/10.1007/978-3-030-48077-6_26
resource representing a document's title	Validating Multiple Variants of an Automotive Light System with Electrum
has PubMed Central identifier	PMC7242091
schema:publication	Rigorous State-Based Methods
resource representing a document's body	covid:259a52b573e278d5279541c5b877c546057301f4#body_text
is schema:about of	named entity 'REFERENCE' named entity 'VARIABILITY' named entity 'temporal logic' named entity 'formal specification language' named entity 'Boolean' named entity 'Boolean' named entity 'neutral element' named entity 'Electrum' named entity 'emergency brake' named entity 'prototype' named entity 'temporal logic' named entity 'state machines' named entity 'arithmetic operations' named entity 'subset' named entity 'prototype' named entity 'Electrum' named entity 'binary relation' named entity 'software products' named entity 'predicate' named entity 'Boolean' named entity 'linear temporal logic' named entity 'Electrum' named entity 'real-time' named entity 'Electrum' named entity 'level of abstraction' named entity 'arithmetic operations' named entity 'relational join' named entity 'input and output' named entity 'real-time' named entity 'daytime running lights' named entity 'pitman arm' named entity 'Electrum' named entity 'user interface' named entity 'algorithm' named entity 'semantics' named entity 'Electrum' named entity 'first-class' named entity 'real-time' named entity 'armoured vehicle' named entity 'Electrum' named entity 'domain experts' named entity 'arity' named entity 'disjunction' named entity 'Electrum' named entity 'model checking' named entity 'graph' named entity 'Cartesian product' named entity 'arity' named entity 'temporal logic' named entity 'real-time' named entity 'predicate' named entity 'first-order' named entity 'tabular data' named entity 'integer' named entity 'Electrum' named entity '3 2 1' named entity 'state machine' named entity 'Electrum' named entity 'state machine' named entity 'SAT solver' named entity 'Electrum' named entity 'regression testing' named entity 'graph' named entity 'state machine' named entity 'Electrum' named entity 'set theory' named entity 'tabular format' named entity 'relational logic' named entity 'steering wheel' named entity 'emergency brake' named entity 'Electrum' named entity 'integer values' named entity 'input and output' named entity 'real-time' named entity 'state machine' named entity 'Electrum' named entity 'validation and verification' named entity 'Electrum' named entity 'user interface' named entity 'Semantically' named entity 'feature model'

Faceted Search & Find service v1.13.91 as of Mar 24 2020

Alternative Linked Data Documents: Sponger | ODE Content Formats:

RDF

ODATA

Microdata

About

OpenLink Virtuoso version 07.20.3229 as of Jul 10 2020, on Linux (x86_64-pc-linux-gnu), Single-Server Edition (94 GB total memory)
Data on this page belongs to its respective rights holders.
Virtuoso Faceted Browser Copyright © 2009-2024 OpenLink Software