mbeddr c: spracherweiterung und formale methodenmbeddr c: spracherweiterung und formale methoden...
TRANSCRIPT
![Page 1: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/1.jpg)
Mbeddr C: Spracherweiterung
und formale Methoden
Markus Voelter independent/itemis
www.voelter.de voelterblog.blogspot.de
@markusvoelter +Markus Voelter
Daniel Ratiu ForTISS GmbH
www.fortiss.org
Bernd Kolb itemis AG
www.itemis.de
@berndkolb +Bernd Kolb
![Page 2: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/2.jpg)
![Page 3: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/3.jpg)
Intro
0
![Page 4: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/4.jpg)
Main Points
More and more software is used in embedded
systems
![Page 5: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/5.jpg)
Main Points
Added-value is driven by software
![Page 6: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/6.jpg)
Main Points
Shorter time to market drives the need for reuse and product
lines
![Page 7: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/7.jpg)
Main Points
As the software – lifespan gets longer,
maintainability becomes more important
![Page 8: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/8.jpg)
Main Points
C does not provide the necessary abstractions
for large scale software engineering
![Page 9: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/9.jpg)
Main Points
At the same time runtime efficiency remains important
![Page 10: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/10.jpg)
So?
![Page 11: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/11.jpg)
What makes developers efficient?
What makes software
maintainable?
![Page 12: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/12.jpg)
![Page 13: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/13.jpg)
And how can a tool and/or language help?
What makes developers efficient?
What makes software maintainable?
![Page 14: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/14.jpg)
Improve Readability if ( tp->alt <= 2000 ) { if ( tp->speed < 150 ) { return 0; } if ( tp->speed >= 150 ) { return 5; } } if ( tp->alt >= 2000 ) { if ( tp->speed < 150 ) { return 10; } if ( tp->speed >= 150 ) { return 20; } }
![Page 15: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/15.jpg)
Improve Readability
![Page 16: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/16.jpg)
Advanced Type Checks
Error: type int32 is not a subtype of int16
![Page 17: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/17.jpg)
Advanced Type Checks
Error: type int16/[m / s] is not a subtype of int16/m
![Page 18: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/18.jpg)
Meaningful Modularity
![Page 19: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/19.jpg)
More Domain Semantics
![Page 20: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/20.jpg)
Better Testability
![Page 21: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/21.jpg)
Higher Level Concepts
![Page 22: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/22.jpg)
Verification
![Page 23: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/23.jpg)
Verification
SUCCESS: Table complete. FAIL: cells (1, 1) and (2, 1) are inconsistent.
tp.alt : 2000 FAIL: cells (1, 2) and (2, 2) are inconsistent.
tp.alt : 2000
![Page 24: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/24.jpg)
Verification
![Page 25: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/25.jpg)
Metadata/Tracing
![Page 26: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/26.jpg)
The Preprocessor
![Page 27: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/27.jpg)
The Preprocessor
![Page 28: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/28.jpg)
![Page 29: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/29.jpg)
![Page 30: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/30.jpg)
![Page 31: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/31.jpg)
All of that without runtime overhead?
![Page 32: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/32.jpg)
![Page 33: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/33.jpg)
mbeddr
1
![Page 34: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/34.jpg)
An extensible version of the C programming language for Embedded Programming
C the Difference – C the Future
gefördert durch das BMBF Förderkennzeichen 01|S11014
![Page 35: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/35.jpg)
An extensible C with support for formal methods, requirements
and PLE.
![Page 36: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/36.jpg)
IDE for Everything
![Page 37: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/37.jpg)
A debugger for all of that
![Page 38: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/38.jpg)
![Page 39: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/39.jpg)
The mbeddr stack
![Page 40: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/40.jpg)
The mbeddr stack
![Page 41: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/41.jpg)
The mbeddr stack
![Page 42: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/42.jpg)
![Page 43: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/43.jpg)
DEMO
![Page 44: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/44.jpg)
![Page 45: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/45.jpg)
Status and
Availability
![Page 46: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/46.jpg)
http://mbeddr.com
![Page 47: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/47.jpg)
LWES Language Workbenches
for Embedded Systems
Developed within
gefördert durch das BMBF Förderkennzeichen 01|S11014
![Page 48: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/48.jpg)
Open Source (Eclipse Public
License)
![Page 49: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/49.jpg)
integration in early / mid
2013
![Page 50: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/50.jpg)
support for graphical mid
2013
![Page 51: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/51.jpg)
First Commercial
Project
![Page 52: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/52.jpg)
2 Developers, 4 months existing source code
30.000 – 50.000 LOC Product Line
Certification Required
![Page 53: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/53.jpg)
Com
m H
AL
App
licat
ion M
etrology U
til
hw-s
peci
fic
DLT645 DLMS/ COSEM
HTTP & TCP/IP
Energy data
Non-Volatile data
Mains frequency measurement
Instantaneous voltage & current sampling
RMS voltage & current calculation
Power & power factor calculation
Energy pulse generation
Energy and consumption calculation
Watch- dog
Clock system
Bin/Bcd converter
LCD formatter
Low-pass filter Ticker
USCI LCD line
Temperature provider RTC Flash
memory Timer ADC10 SD24 E²PROM
PLC modem
Energy data display
Multi-tariff & billing periods
support
Magnetic interference protection
DLT645 calibration commands
Load profile support
Time of use Reset function, historical data
recording
COSEM objects/OBIS
codes
Anti-tampering/ anti-fraud
Last/average/maximum demand
Output relay control
hard
war
e-in
depe
nden
t
Software Layers & Components
![Page 54: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/54.jpg)
Systematic Study with
BMW
![Page 55: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/55.jpg)
The “Pacemaker” Challenge
![Page 56: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/56.jpg)
![Page 57: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/57.jpg)
Formal Verification
2
![Page 58: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/58.jpg)
Challenge: adoption of formal verification in
practice
![Page 59: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/59.jpg)
Who uses Formal Verification?
Big companies and organizations IBM, NASA, Intel, Airbus, Boeing, Microsoft, ...
Safety critical systems Development of flight controllers, processors,
control units of nuclear power plants, automatic trains, ...
Projects with big budgets, long life-cycle Development spans over years, teams of experts are available
![Page 60: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/60.jpg)
What about small and medium enterprises?
![Page 61: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/61.jpg)
What about small and medium enterprises?
Often FV is seen as expert tools,
too heavy weighted, too expensive,
not practicable …
![Page 62: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/62.jpg)
Our goal: formal verification
for everyone
![Page 63: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/63.jpg)
Easy to understand Easy to learn Easy to use
. . . by non computer-
scientists
![Page 64: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/64.jpg)
Short round-trip for defining checks, performing analysis,
and interpreting results.
![Page 65: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/65.jpg)
Integrate formal verification
in more agile processes
Continuously define run and interpret formal analyses
![Page 66: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/66.jpg)
1) Writing the formal model
2) Specify the property to be verified 3) Interpret the analysis results
Challenges with using formal analyses
![Page 67: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/67.jpg)
Addressing the 1) Wrap the language of the
analysis tool into higher level languages
2) Define out-of-the-box analyses goals that can be automated
3) Lift the analysis results at the abstraction level of the domain
Challenges
![Page 68: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/68.jpg)
Analyses are simpler to define
Automation degree grows / analyses are (computationally)
more feasible
The results of analyses can be presented in more adequate form
Adequate Languages Make Life Simpler
![Page 69: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/69.jpg)
Today’s state of practice: Write some program (e.g. C) and then try (very hardly) to analyze it.
Adequate Languages Make Life Simpler
![Page 70: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/70.jpg)
Today’s state of practice: Write some program (e.g. C) and then try (very hardly) to analyze it.
Today’s state of the art: Write programs that can be analyzed
Adequate Languages Make Life Simpler
![Page 71: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/71.jpg)
Today’s state of practice: Write some program (e.g. C) and then try (very hardly) to analyze it.
The mbeddr approach: … by using adequate language (fragments)
Today’s state of the art: Write programs that can be analyzed
Adequate Languages Make Life Simpler
![Page 72: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/72.jpg)
Code-based, Model-based and DSLs-based Analyses
Formal analysis tools – e.g. model checkers, SMT solvers
GPL Code
GPL Code
Abstract models
Abstraction
Program abstraction
Generation
C code
DSL1 DSL2 ... DSL3
Clean, easy to analyze DSLs
![Page 73: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/73.jpg)
73
Allow Software Developers Make Informed Decisions
Either write a sub-system in a restricted (but verifiable)
language
![Page 74: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/74.jpg)
74
Allow Software Developers Make Informed Decisions
Either write a sub-system in a restricted (but verifiable)
language or
use the full power of a GPL
![Page 75: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/75.jpg)
75
Allow Software Developers Make Informed Decisions
Either write a sub-system in a restricted (but verifiable)
language or
use the full power of a GPL
and: get immediate feedback if you are
(not) in the verifiable sub-set
![Page 76: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/76.jpg)
Characteristics of Analyzable Languages
High modularisation and encapsulation Small and well-defined interfaces
Clean-up or restrict „problematic“ features Access to global state, side-effects, etc.
Raise the level of abstraction Be able to leave out unnecessary details
Eliminate the „accidental complexity“ Be able to directly express what we want
without any „encoding“ 76
![Page 77: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/77.jpg)
… for analyses users:
Paradigm Change
decide which parts of programs will be analyzed and use
adequate language fragments that allow analysis
![Page 78: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/78.jpg)
![Page 79: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/79.jpg)
Verifying Decision Tables
Referencing
![Page 80: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/80.jpg)
Decision Tables
![Page 81: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/81.jpg)
Completeness: did we cover all cases? Consistency: are there overlapping cases?
Decision Tables
![Page 82: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/82.jpg)
Predicates Delimit Regions in the Variables Space
P1
P2
P3
![Page 83: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/83.jpg)
Completeness = do we cover the whole space?
P1 P2
X < 0 X >= 0 Complete
Incomplete
Formulating as SAT problem: if „not (P1 or P2)“ is SAT then the
decision table is incomplete
![Page 84: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/84.jpg)
Consistency = are the regions overlapping?
P1 P2
Consistent
Incosistent
P1 P2
Formulating as SAT problem: is „P1 and P2“ satisfiable? If yes, then table cells are active at the same time
![Page 85: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/85.jpg)
Easy to answer automatically using an SMT solver J
SMT = Satisfiability Modulo Theories
- extension of boolean satisfiability with additional theories like linear arithmetic
![Page 86: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/86.jpg)
Decision Tables
![Page 87: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/87.jpg)
Language restriction: non-linear expressions
are not allowed
Decision Tables
![Page 88: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/88.jpg)
![Page 89: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/89.jpg)
Verifying Feature Models
Referencing
![Page 90: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/90.jpg)
Feature Models
![Page 91: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/91.jpg)
Can this feature model be instantiated?
Feature Models
![Page 92: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/92.jpg)
Does this configuration comply to the feature model?
Feature Models
![Page 93: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/93.jpg)
Feature Models
“SAT-based analyses of feature models are easy!”
[Mendoca et. al., SPLC’09 ]
![Page 94: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/94.jpg)
Behind the Scene (set-evidence! true) (set-verbosity! 2) ;; each feature is declared as a boolean variable (define root::bool) (define Diagnosis::bool) (define Logging::bool) ... ; the root feature is always present (assert root) ;; for each (sub-feature, feature) we have "sub-feature -> feature" (assert (or (not Diagnosis) root) ) (assert (or (not Logging) Diagnosis) ) (assert (or (not HeartBeat) Diagnosis) ) ... ;; for each mandatory sub-feature we have "feature -> sub-feature" (assert+ (or (not root) Diagnosis) ) (assert+ (or (not root) DataAquisition) ) (assert+ (or (not root) CommProtocol) )
![Page 95: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/95.jpg)
Raw Results
Raw result unsat unsat core ids: 1 3 5 7 9 10
![Page 96: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/96.jpg)
Lifted Results
![Page 97: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/97.jpg)
![Page 98: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/98.jpg)
Verifying State
Machines
Referencing
![Page 99: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/99.jpg)
Model Checking
![Page 100: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/100.jpg)
Model Checking
![Page 101: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/101.jpg)
Model Checking
![Page 102: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/102.jpg)
Model Checking
![Page 103: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/103.jpg)
Model Checking
![Page 104: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/104.jpg)
Unreachable States Dead End States
Live States
Out of the box verification conditions
Transitions Nondeterminism
Dead Transitions
Variables out-of-bounds
Check the sanity of the code
![Page 105: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/105.jpg)
Have a (temporal) scope: Global
Before R
After Q
Between Q and R
After Q Until R
User Defined Properties
Define Business-Domain Specific Verification Conditions
… that restrict a certain basic property:
P not P S responds to P
R R
Q Q
Q Q R R Q Q
Q Q R Q
![Page 106: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/106.jpg)
![Page 107: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/107.jpg)
![Page 108: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/108.jpg)
![Page 109: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/109.jpg)
Checking contracts of components
Referencing
![Page 110: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/110.jpg)
Contracts
Define what an interface expects and promisses from/to its environment
Preconditions (assumptions)
Postconditions (guarantees)
![Page 111: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/111.jpg)
Contracts
Does this client comply with the interface?
![Page 112: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/112.jpg)
Checking Contracts
Problem: the variable „time“ can be zero.
![Page 113: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/113.jpg)
How is this done? Reduce the analysis to reacheability.
- For each pre/postcondition we generate a label - Use the CBMC model checker to check the code. - Lift the counterexample at the DSL level
![Page 114: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/114.jpg)
![Page 115: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/115.jpg)
Checking interface
protocols of components
Referencing
![Page 116: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/116.jpg)
Interface Protocols
Define an order upon the execution of operations
... E.g. before ‚drive‘ can be called the system must be in the state ‚Running‘ ... to change the direction we first must stop
![Page 117: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/117.jpg)
Interface Protocols
Which sequence of operations is allowed?
![Page 118: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/118.jpg)
Interface Protocols
Before reversing the direction we must stop
![Page 119: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/119.jpg)
![Page 120: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/120.jpg)
Extending Mbeddr
3
![Page 121: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/121.jpg)
Extensibility Prevent users from using forbidden constructs
• MISRA • Void-Pointers • Pointer Arithmatics • …
all depending on your context
![Page 122: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/122.jpg)
Extensibility Prevent users from using forbidden constructs
• MISRA • Void-Pointers • Pointer Arithmatics • …
all depending on your context
Add custom types • (arbitrary precision) fixed point • OS-Types such as TASK or EVENT • Vectors, Matrices • …
with support for custom validations and special operators
![Page 123: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/123.jpg)
Extensibility Prevent users from using forbidden constructs
• MISRA • Void-Pointers • Pointer Arithmatics • …
all depending on your context
Add custom types • (arbitrary precision) fixed point • OS-Types such as TASK or EVENT • Vectors, Matrices • …
with support for custom validations and special operators
Custom language extensions • acquire memory, do reference counting and garbage collection
• state machines • …
![Page 124: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/124.jpg)
Extensibility Prevent users from using forbidden constructs
• MISRA • Void-Pointers • Pointer Arithmatics • …
all depending on your context
Add custom types • (arbitrary precision) fixed point • OS-Types such as TASK or EVENT • Vectors, Matrices • …
with support for custom validations and special operators
Custom language extensions • acquire memory, do reference counting and garbage collection
• statemachines • …
Tool Integration • Requirements • Verification Tools • Build Tools • …
as first class citizen
![Page 125: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/125.jpg)
more specialized domains more specialized languages
Extension Extension
![Page 126: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/126.jpg)
more specialized domains more specialized languages
Extension Extension
![Page 127: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/127.jpg)
more specialized domains more specialized languages
Extension Extension
![Page 128: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/128.jpg)
more specialized domains more specialized languages
Extension Extension
![Page 129: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/129.jpg)
C
LEGO Robot Control
Components
State Machines
Sensor Access
General Purpose
Domain Specific
![Page 130: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/130.jpg)
my L
α
β
a b c
d e f
g h i
j k l
Modular Language
composable modules with many optional,
![Page 131: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/131.jpg)
![Page 132: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/132.jpg)
Incremental Trafo
![Page 133: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/133.jpg)
Incremental Trafo
![Page 134: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/134.jpg)
Incremental Trafo
![Page 135: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/135.jpg)
Incremental Trafo
![Page 136: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/136.jpg)
![Page 137: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/137.jpg)
A Language Extension
Concept Tooling Semantics
Editor Validations Refactoring
Typesystem
Generator
![Page 138: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/138.jpg)
Assign fixed types
What does a type system do?
![Page 139: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/139.jpg)
Assign fixed types
Derive Types
What does a type system do?
![Page 140: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/140.jpg)
Assign fixed types
Derive Types
Calculate Common Types
What does a type system do?
![Page 141: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/141.jpg)
Assign fixed types
Derive Types
Calculate Common Types
Check Type Consistency
What does a type system do?
![Page 142: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/142.jpg)
![Page 143: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/143.jpg)
Recap
4
![Page 144: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/144.jpg)
Main Points
Meaningful abstractions help to build maintainable
software.
![Page 145: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/145.jpg)
Main Points
Abstractions without good tool support don’t
work with most developers. Tool
integration is key.
![Page 146: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/146.jpg)
Main Points Once programs contain
(domain-specific) abstractions,
meaningful formal analyses can be
performed much more easily.
![Page 147: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/147.jpg)
Main Points
When integrated directly into the IDE
every project can benefit without big additional effort.
![Page 148: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/148.jpg)
Main Points Mbeddr is an open,
extensible language workbench which can help you to overcome
your software engineering problems
![Page 149: Mbeddr C: Spracherweiterung und formale MethodenMbeddr C: Spracherweiterung und formale Methoden Markus Voelter independent/itemis voelter@acm.org voelterblog.blogspot.de @markusvoelter](https://reader035.vdokument.com/reader035/viewer/2022071216/604714c20817a87d2b538c0b/html5/thumbnails/149.jpg)