Fallstudien

Auf dieser Seite sind die verschiedenen in AVACS untersuchten Fallstudien zu finden. Auf einige dieser Fallstudien kann nur mit Passwort zugegriffen werden. Diese sind mit PP gekennzeichnet.

Benchmarks Phase 2

Name

Benutzt in

PP

Beschreibung

Modell

Approach Velocity Controller

H3

no

Beschreibung

Modell

Bouncing Balls

H4

no

Beschreibung

Modell

Bounded Retransmission Protocol

S2

no

Beschreibung

Modell (einfach und modular)

Bounded Retransmission Protocol

S3

no

Beschreibung

Modell

Blackbox BMC Suite

S1, H1/2

yes

Beschreibung

Modell

Chord Network

S3

yes

Beschreibung

Modell

Contract Signing Protokoll

S3

yes

Beschreibung

Modell

Crowds Protokoll

S3

yes

Beschreibung

Modell

CSMACD

S2

no

Beschreibung

Modell

Dam

H3

no

Beschreibung

Modell

Dam (Extended)

H3

yes

Beschreibung

Modell

Erlang Stages

S3

no

Beschreibung

Modell

ETCS Emergency Messages

R1

yes

Beschreibung

Modell

ETCS Example

H3

yes

ATR 54

Modell

ETCS Train System

H1/2

no

Beschreibung

Modell

Flap/Slat System

H3

no

Beschreibung

Modell

iSAT-LP Benchmarks

H1/2

yes

Beschreibung

Modell

iSAT-Craig Benchmarks

H1/2

yes

Bechreibung

Modell

iSAT-ODE Benchmarks

H1/2

no

Beschreibung

Modell

iSAT Traffic Benchmarks

H1/2

no

ATR 81

Modell

Jackson Queues

S3

no

Beschreibung

Modell

Lane Change Assistant

H3

yes

ATR 78

Modell

Lawn Mover

H4

no

Beschreibung

Modell

Mastermind

S3

no

Beschreibung

n.a.

Moving Block Train Control

H4

no

Beschreibung

Modell A und B

Networked Automation System (for SiSAT)

H1/2

yes

Beschreibung

Modell

Networked Control System

H1/2

no

Beschreibung

Modell

Protein Synthesis

S3

no

Beschreibung

Modell

Quasi-Birth-Death Processes

S3

no

Beschreibung

Modell

Railroad Crossing

H3

no

Beschreibung

Modell

Random Walk

S3

no

Beschreibung

Modell

Randomized Consensus

S3

no

Beschreibung

Modell

Randomized Mutual Exclusion

S3

no

Beschreibung

Modell

Randomized Scheduling

S3

no

Beschreibung

n.a.

RBC Complex Topologies

R1

no

ATR 66

Modell

RCAS Example

H3

yes

n.a.

Modell

Stochastic Job Scheduling

S3

no

Beschreibung

Modell

Synchronous Leader Election Protocol

S3

yes

Beschreibung

Modell

SPASS(iSAT) Benchmarks

H1/2

yes

Beschreibung

Modell

SPASS(Z3) Benchmarks

H1/2

yes

Beschreibung

Modell

Self-stabilizing Minimal Spanning Tree

S3

yes

Beschreibung

Modell

Tandem Queues

S3

no

Beschreibung

Modell

Temperature Control

H4

no

Beschreibung

Modell

Thermostat

H4

no

Beschreibung

Modell

Timed Blackbox BMC Suite

S1

yes

Beschreibung

Modell

Two Tank System (iSAT(ODE))

H1/2

yes

Beschreibung

Modell

ViDAS

R2

yes

Beschreibung

Modell

Water Level Control

H4

no

Beschreibung

Modell

Water Level Control (HSCC'11)

H4

no

Beschreibung

Modell A, B, C und D

Wireless LAN

S2

no

Beschreibung

Modell

Workstation Cluster

S3

no

Beschreibung

Modell

Zeroconf

S3

no

Beschreibung

Modell

External

Link to

Hardware Model Checking Competition benchmark set 2008

H1/2

Externer Link

Hardware Model Checking Competition benchmark set 2010

H1/2

Externer Link

H-PILoT

R1, H3

Externer Link (Download)

HSolver Benchmarks

H1/2

Sourceforge

HySAT Benchmarks

H1/2

Externer Link

iSAT Benchmarks

H1/2

GForge

LIRA Benchmarks

H1/2

Benchmark und einfache Dokumentation in GForge

Mälardalen Benchmarks

R2

Externer Link

QBFLIB

S1

Externer Link

SAT Competition Benchmarks

H1/2

Externer Link

SMT-LIB

H1/2, R1

Externer Link

 

 

 

 

 

Benchmarks Phase 1

Name

Benutzt in

PP

Beschreibung

Modell

Air Conditioner System

Rl

yes

Beschreibung

Modell

Aircraft Collision Avoidance Protocol

H1/2

no

Beschreibung

Modell

Arbiter

R3

no

Beschreibung

n.a.

Automated Rail Cars System

S2

yes

Beschreibung

Modell

Automatic Task Allocation in Distributed Systems

R2

yes

Beschreibung

n.a.

Car Platooning

S2

yes

Beschreibung

Modell

Car Window Lifting

H3

yes

Beschreibung

Modell

Elastic Train Control

H1/2

no

Beschreibung

n.a.

Emergency Messages in ETCS

R1

yes

Beschreibung

Modell

ETCS Application Level 2

S3

no

Beschreibung

n.a.

ETCS Break Risk Assessment

S3

no

Beschreibung

n.a.

ETCS Level 3

S2

yes

Beschreibung

n.a.

Fault-Tolerant Workstation Cluster

S3

no

Beschreibung

n.a.

FFB

S1

yes

Beschreibung

Modell

Fischer Protocol

R3

yes

Beschreibung

Modell

Flap controller

H3

no

Beschreibung

n.a.

Flexray

S1

no

n.a.

Modell

Flight Control System

H3

yes

Beschreibung

Modell

Formats

S1

no

n.a

Modell

Garay/MacKenzie Protocol

S1

yes

Beschreibung

Modell

GPS Controller

S1, R3

no

n.a

Modell

GPS Controller 2

S1, R3

no

n.a

Modell

Hanoi

R3

no

Beschreibung

n.a.

Kanban Production System

S3

no

Beschreibung

n.a.

Mutual Exclusion

R3

yes

Beschreibung

Modell

Mutual Exclusion with Random Times

S3

no

Beschreibung

n.a.

Pipelined ALU

S1

yes

Beschreibung

Modell

Production Cell

S1

no

n.a

Modell

Region Stable Hybrid Systems

H4

no

Beschreibung

n.a.

RTSS'10

R2

no

n.a.

Modell

Single-tracked Line Segment

R3

yes

Beschreibung

Modell

SLAB Benchmarks

R1

no

Beschreibung

n.a.

Sliding Window

S1

yes

Beschreibung

Modell

Stable Drive Train

H4

yes

Beschreibung

n.a.

Stable Ordinary Differential Equations

H4

no

Beschreibung

n.a.

Trainsystem

Projektbereich H, insbesondere H3

yes

Beschreibung

Matlab Modell

VIS Benchmarks

S1

no

Beschreibung

n.a.

VLIW ALU

S1

yes

Beschreibung

Modell

External

Link to

HSolver Benchmarks

Sourceforge