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

Automatic Verification And Analysis of Complex Systems

Menü

Fallstudien

Benchmarks Phase 2

Benchmarks Phase 1