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 Plus annual

Presents the access of premium content as premium feature

Premium Content

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 Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

Model checking real-time systems is complex, and requires a careful trade-offbetween including enough detail to be useful and not too much detail to avoidstate explosion. This work exploits variability of the formal model beinganalysed and the requirements being checked, to facilitate the model-checkingof variations of real-time specifications. This work results from thecollaboration between academics and Alstom, a railway company with a concreteuse-case, in the context of the VALU3S European project. The configuration ofthe variability of the formal specifications is described in MS Excelspreadsheets with a particular structure, making it easy to use also bydevelopers. These spreadsheets are processed automatically by our prototypetool that generates instances and runs the model checker. We propose theextension of our previous work by exploiting analysis over valid combination offeatures, while preserving the simplicity of a spreadsheet-based interface withthe model checker.

Spreadsheet-based Configuration of Families of Real-Time Specifications