Dr. rer. nat. Dimitri Bohlender

Kontakt

Wissenschaftlicher Mitarbeiter

Tel. +49 241 80 21174
Fax +49 241 80 22150

Adresse: Ahornstr. 55, 52074 Aachen, Germany
Büro: Raum 2302 (Gebäude H, 3.OG)

Email: bohlender[at]embedded[dot]rwth-aachen[dot]de
Web: bohlender.pro

Offene Abschlussarbeiten

Aktuell liegen keine ausformulierten, offenen Abschlussarbeiten vor. Bei Interesse an formalen Methoden können wir aber zusammen geeignete Themen für Bachelor- und Masterarbeiten ausarbeiten. Eigene Vorschläge sind ebenfalls möglich.

Lehre

Semester	Titel	Art
WS 19/20	Proseminar: Grundlagen eingebetteter Systeme	S
SS 19	Seminar: Ausgesuchte Themen zur Eingebetteten Software	S
SS 19	Proseminar: Grundlagen eingebetteter Systeme	S
WS 18/19	Formale Methoden für Steuerungssoftware	V
WS 18/19	Formale und semiformale Methoden für eingebettete Software	S
SS 18	Formale und semiformale Methoden für eingebettete Software	S
WS 17/18	Formale Methoden für Steuerungssoftware	V
WS 17/18	Formale und semiformale Methoden für eingebettete Software	S
SS 17	Formale und semiformale Methoden für eingebettete Software	S
WS 16/17	Formale Methoden für Steuerungssoftware	V
SS 16	Formale und semiformale Methoden für eingebettete Software	S
WS 15/16	Formale Methoden für Steuerungssoftware	V
WS 15/16	Formale und semiformale Methoden für eingebettete Software	S
SS 15	Formale und semiformale Methoden für eingebettete Software	S

Publikationen

Publikations-Export

[Boh21] PDF BIB

Bohlender, D., "Symbolic methods for formal verification of industrial control software", PhD Thesis, Aachen, 2021.

Symbolic methods for formal verification of industrial control software

Bibtex entry :

@phdthesis {  Boh21,
	author = { Bohlender, Dimitri },
	othercontributors = { Kowalewski, Stefan and Hermanns, Holger },
	title = { Symbolic methods for formal verification of industrial
		control software },
	publisher = { RWTH Aachen University },
	school = { RWTH Aachen University },
	pages = { 1 Online-Ressource : Illustrationen, Diagramme },
	series = { Aachener Informatik-Berichte },
	year = { 2021 },
	address = { Aachen },
	doi = { 10.18154/RWTH-2021-10633 },
	typ = { PUB:(DE-HGF)11 },
	reportid = { RWTH-2021-10633 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/835546/files/835546.pdf },
}

[GSB+20] PDFBIB

Grochowski, M., Simon, H., Bohlender, D., Kowalewski, S., Löcklin, A., Müller, T., Jazdi, N., Zeller, A., and Weyrich, M., "Formale Methoden für rekonfigurierbare cyber-physische Systeme in der Produktion", Automatisierungstechnik, vol. 68, iss. 1, pp. 3-14, 2020

Formale Methoden für rekonfigurierbare cyber-physische Systeme in der Produktion

Bibtex entry :

@article {  GSB+20,
	author = { Grochowski, Marco and Simon, Hendrik and Bohlender, Dimitri
		and Kowalewski, Stefan and L{\"o}cklin, Andreas and
		M{\"u}ller, Timo and Jazdi, Nasser and Zeller, Andreas and
		Weyrich, Michael },
	title = { Formale Methoden f{\"u}r rekonfigurierbare cyber-physische
		Systeme in der Produktion },
	journal = { Automatisierungstechnik },
	publisher = { De Gruyter },
	pages = { 3-14 },
	volume = { 68 },
	number = { 1 },
	year = { 2020 },
	address = { Berlin },
	issn = { 2196-677X },
	doi = { 10.1515/auto-2019-0115 },
	typ = { PUB:(DE-HGF)16 },
	reportid = { RWTH-2019-12214 },
	cin = { 122810 / 120000 },
}

[BCK+19] PDF BIB

Bohlender, D., Chiyah Garcia, F. J., Köhl, M., Menghi, C., and Wortmann, A., "On Explainability and its Characterization", , pp. 4-7, 2019

On Explainability and its Characterization

Bibtex entry :

@article {  BCK+19,
	author = { Bohlender, Dimitri and Chiyah Garcia, Francisco J. and
		K{\"o}hl, Maximilian and Menghi, Claudio and Wortmann,
		Andreas },
	title = { On Explainability and its Characterization },
	pages = { 4-7 },
	year = { 2019 },
	organization = { GI Dagstuhl Seminar 19023 on Explainable Software for
		Cyber-Physical Systems, Dagstuhl (Germany), 2019-01-06 -
		2019-01-11 },
	doi = { 10.18154/RWTH-2020-01625 },
	typ = { PUB:(DE-HGF)25 },
	reportid = { RWTH-2020-01625 },
	cin = { 122810 / 120000 / 121510 },
	url = { https://arxiv.org/pdf/1904.11851.pdf#page=9 },
}

[BK19] PDF BIB

Bohlender, D. and Kowalewski, S., "Leveraging Horn clause solving for compositional verification of PLC software", Discrete event dynamic systems, vol. 30, pp. 1-24, 2019

Leveraging Horn clause solving for compositional verification of PLC software

Bibtex entry :

@article {  BK19,
	author = { Bohlender, Dimitri and Kowalewski, Stefan },
	title = { Leveraging Horn clause solving for compositional
		verification of PLC software },
	journal = { Discrete event dynamic systems },
	publisher = { Springer Science + Business Media B.V },
	pages = { 1-24 },
	volume = { 30 },
	year = { 2019 },
	address = { Dordrecht [u.a.] },
	issn = { 1573-7594 },
	doi = { 10.1007/s10626-019-00296-8 },
	typ = { PUB:(DE-HGF)16 },
	reportid = { RWTH-2019-12207 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/775404 },
}

[BK19a] PDF BIB

Bohlender, D. and Köhl, M. A., "Towards a Characterization of Explainable Systems", , 2019

Towards a Characterization of Explainable Systems

Bibtex entry :

@article {  BK19a,
	author = { Bohlender, Dimitri and K{\"o}hl, Maximilian A. },
	title = { Towards a Characterization of Explainable Systems },
	year = { 2019 },
	typ = { PUB:(DE-HGF)25 },
	reportid = { RWTH-2020-01624 },
	cin = { 122810 / 120000 },
	url = { https://www.semanticscholar.org/paper/Towards-a-Characterization-of-Explainable-Systems-Bohlender-K%C3%B6hl/b3516a71fed895a1a88b7d9842eca41c0fb48b7d },
}

[KBL+19] PDF BIB

Köhl, M. A., Baum, K., Langer, M., Oster, D., Speith, T., and Bohlender, D., "Explainability as a Non-Functional Requirement", in Proc. 2019 IEEE 27th International Requirements Engineering Conference : 23-27 September 2019, Jeju Island, South Korea : proceedings / editors: Daniela Damian and Anna Perini (Program Chairs), Seok-Won Lee (General Chair), Piscataway, JN, 2019, IEEE, pp. 363-368.

Explainability as a Non-Functional Requirement

Bibtex entry :

@inproceedings {  KBL+19,
	author = { K{\"o}hl, Maximilian A. and Baum, Kevin and Langer, Markus
		and Oster, Daniel and Speith, Timo and Bohlender, Dimitri },
	title = { Explainability as a Non-Functional Requirement },
	booktitle = { 2019 IEEE 27th International Requirements Engineering
		Conference : 23-27 September 2019, Jeju Island, South Korea
		: proceedings / editors: Daniela Damian and Anna Perini
		(Program Chairs), Seok-Won Lee (General Chair) },
	publisher = { IEEE },
	pages = { 363-368 },
	year = { 2019 },
	address = { Piscataway, JN },
	organization = { IEEE 27. International Requirements Engineering Conference,
		Jeju Island (South Korea), 2019-09-23 - 2019-09-27 },
	doi = { 10.1109/RE.2019.00046 },
	typ = { PUB:(DE-HGF)7 },
	reportid = { RWTH-2019-12206 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/775403 },
}

[BHK18] PDF BIB

Bohlender, D., Hamm, D., and Kowalewski, S., "Cycle-Bounded Model Checking of PLC Software via Dynamic Large-Block Encoding", in Proc. Applied computing 2018 : the 33rd Annual ACM Symposium on Applied Computing : Pau, France, April 9-13, 2018 / sponsored by: ACM Special Interest Group on Applied Computing ; conference chairs: Hisham M. Haddad (Kennesaw State University, USA), Roger L. Wainwright (University of Tulsa, USA), Richard Chbeir (University of Pau & Pays Adour, France), New York, NY, 2018, ACM, pp. 1891-1898.

Cycle-Bounded Model Checking of PLC Software via Dynamic Large-Block Encoding

Bibtex entry :

@inproceedings {  BHK18,
	author = { Bohlender, Dimitri and Hamm, Daniel and Kowalewski, Stefan },
	title = { Cycle-Bounded Model Checking of PLC Software via Dynamic
		Large-Block Encoding },
	booktitle = { Applied computing 2018 : the 33rd Annual ACM Symposium on
		Applied Computing : Pau, France, April 9-13, 2018 /
		sponsored by: ACM Special Interest Group on Applied
		Computing ; conference chairs: Hisham M. Haddad (Kennesaw
		State University, USA), Roger L. Wainwright (University of
		Tulsa, USA), Richard Chbeir (University of Pau & Pays Adour,
		France) },
	publisher = { ACM },
	pages = { 1891-1898 },
	year = { 2018 },
	address = { New York, NY },
	organization = { 33. ACM Symposium on Applied Computing, Pau (France),
		2018-04-09 - 2018-04-13 },
	doi = { 10.1145/3167132.3167334 },
	typ = { PUB:(DE-HGF)7 },
	reportid = { RWTH-2018-231950 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/752221 },
}

[BK18] PDF BIB

Bohlender, D. and Kowalewski, S., "Compositional Verification of PLC Software using Horn Clauses and Mode Abstraction", IFAC-PapersOnLine, vol. 51, iss. 7, pp. 428-433, 2018

Compositional Verification of PLC Software using Horn Clauses and Mode Abstraction

Bibtex entry :

@article {  BK18,
	author = { Bohlender, Dimitri and Kowalewski, Stefan },
	title = { Compositional Verification of PLC Software using Horn
		Clauses and Mode Abstraction },
	journal = { IFAC-PapersOnLine },
	pages = { 428-433 },
	volume = { 51 },
	number = { 7 },
	year = { 2018 },
	address = { Laxenburg },
	issn = { 2405-8963 },
	organization = { 14. IFAC International Workshop on Discrete Event Systems,
		Castellammare di Stabia (Italy), 2018-05-30 - 2018-06-01 },
	doi = { 10.1016/j.ifacol.2018.06.336 },
	typ = { PUB:(DE-HGF)16 },
	reportid = { RWTH-2018-227071 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/730763 },
}

[BK18a] PDF BIB

Bohlender, D. and Kowalewski, S., "Design and Verification of Restart-Robust Industrial Control Software", in Proc. Integrated formal methods : 14th International Conference, IFM 2018, Maynooth, Ireland, September 5-7, 2018 : proceedings / Carlo A. Furia, Kirsten Winter (eds.), Cham, 2018 in Lecture notes in computer science, Springer, pp. 47-68.

Design and Verification of Restart-Robust Industrial Control Software

Bibtex entry :

@inproceedings {  BK18a,
	author = { Bohlender, Dimitri and Kowalewski, Stefan },
	title = { Design and Verification of Restart-Robust Industrial Control
		Software },
	booktitle = { Integrated formal methods : 14th International Conference,
		IFM 2018, Maynooth, Ireland, September 5-7, 2018 :
		proceedings / Carlo A. Furia, Kirsten Winter (eds.) },
	publisher = { Springer },
	pages = { 47-68 },
	series = { Lecture notes in computer science },
	year = { 2018 },
	address = { Cham },
	organization = { 14. International Conference on Integrated Formal Methods,
		Maynooth (Ireland), 2018-09-05 - 2018-09-07 },
	doi = { 10.1007/978-3-319-98938-9_4 },
	typ = { PUB:(DE-HGF)7 },
	reportid = { RWTH-2018-231948 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/752219 },
}

[UVS+17] PDF BIB

Ulewicz, S., Vogel-Heuser, B., Simon, H., Bohlender, D., Obster, M., and Kowalewski, S., "A priori test coverage estimation for automated production systems : Using generated behavior models for coverage calculation", in Proc. 2017 22nd IEEE International Conference on Emerging Technologies and Factory Automation : September 12-15, 2017, Limassol, Cyprus / ABB, IEEE, IES, University of Cyprus, Piscataway, NJ, 2017, IEEE, p. 4.

A priori test coverage estimation for automated production systems : Using generated behavior models for coverage calculation

Bibtex entry :

@inproceedings {  UVS+17,
	author = { Ulewicz, Sebastian and Vogel-Heuser, Birgit and Simon,
		Hendrik and Bohlender, Dimitri and Obster, Mathias and
		Kowalewski, Stefan },
	title = { A priori test coverage estimation for automated production
		systems : Using generated behavior models for coverage
		calculation },
	booktitle = { 2017 22nd IEEE International Conference on Emerging
		Technologies and Factory Automation : September 12-15, 2017,
		Limassol, Cyprus / ABB, IEEE, IES, University of Cyprus },
	publisher = { IEEE },
	pages = { 4 Seiten },
	year = { 2017 },
	address = { Piscataway, NJ },
	organization = { 22. IEEE International Conference on Emerging Technologies
		and Factory Automation, Limassol (Cyprus), 2017-09-12 -
		2017-09-15 },
	doi = { 10.1109/ETFA.2017.8247704 },
	typ = { PUB:(DE-HGF)7 },
	reportid = { RWTH-2018-223451 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/722217 },
}

[BSF+16] PDF BIB

Bohlender, D., Simon, H., Friedrich, N., Kowalewski, S., and Hauck-Stattelmann, S., "Concolic test generation for PLC programs using coverage metrics", in Proc. 2016 13th International Workshop on Discrete Event Systems (WODES) : May 30-June 1, 2016, Xi'an, China / edited by Christos G. Cassandras, Alessandro Giua, Zhiwu Li ; sponsored by IEEE - Control Systems Society, Piscataway, NJ, 2016, IEEE, pp. 432-437.

Concolic test generation for PLC programs using coverage metrics

Bibtex entry :

@inproceedings {  BSF+16,
	author = { Bohlender, Dimitri and Simon, Hendrik and Friedrich, Nico
		and Kowalewski, Stefan and Hauck-Stattelmann, Stefan },
	title = { Concolic test generation for PLC programs using coverage
		metrics },
	booktitle = { 2016 13th International Workshop on Discrete Event Systems
		(WODES) : May 30-June 1, 2016, Xi'an, China / edited by
		Christos G. Cassandras, Alessandro Giua, Zhiwu Li ;
		sponsored by IEEE - Control Systems Society },
	publisher = { IEEE },
	pages = { 432-437 },
	year = { 2016 },
	address = { Piscataway, NJ },
	organization = { 13. International Workshop on Discrete Event Systems, Xi'an
		(Peoples R China), 2016-05-30 - 2016-06-01 },
	doi = { 10.1109/WODES.2016.7497884 },
	typ = { PUB:(DE-HGF)7 },
	reportid = { RWTH-2016-11193 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/679431 },
}

[BSK+16] PDF BIB

Bohlender, D., Simon, H., Kowalewski, S., and Hauck-Stattelmann, S., "Symbolische Ausführung zum Testen von SPS-Programmen", in Proc. Automation 2016 : secure & reliable in the digital world : 17. Branchentreff der Mess- und Automatisierungstechnik : Baden-Baden, 07. und 08. Juni 2016 / VDI/VDE Mess- und Automatisierungstechnik, Düsseldorf, 2016 in VDI-Berichte, VDI Verlag GmbH, pp. 13-14.

Symbolische Ausführung zum Testen von SPS-Programmen

Bibtex entry :

@inproceedings {  BSK+16,
	author = { Bohlender, Dimitri and Simon, Hendrik and Kowalewski, Stefan
		and Hauck-Stattelmann, S. },
	title = { Symbolische Ausf{\"u}hrung zum Testen von SPS-Programmen },
	booktitle = { Automation 2016 : secure & reliable in the digital world :
		17. Branchentreff der Mess- und Automatisierungstechnik :
		Baden-Baden, 07. und 08. Juni 2016 / VDI/VDE Mess- und
		Automatisierungstechnik },
	publisher = { VDI Verlag GmbH },
	pages = { 13-14 },
	series = { VDI-Berichte },
	year = { 2016 },
	address = { D{\"u}sseldorf },
	organization = { 17. Branchentreff der Mess- und Automatisierungstechnik,
		Baden-Baden (Germany), 2016-06-07 - 2016-06-08 },
	typ = { PUB:(DE-HGF)7 },
	reportid = { RWTH-2016-12035 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/680852 },
}

[BSK16] PDF BIB

Bohlender, D., Simon, H., and Kowalewski, S., "Symbolic verification of PLC safety-applications based on PLCopen automata", in Proc. MBMV 2016 : 19. GI/ITG/GMM-Workshop "Methoden und Beschreibungsprachen zur Modellierung und Verifikation von Schaltungen und Systemen" : Albert-Ludwigs-Universität Freiburg im Breisgau 1.–2. März 2016 / Ralf Wimmer (Herausgeber), Freiburg im Breisgau, 2016, Albert-Ludwigs-Universität, pp. 33-45.

Symbolic verification of PLC safety-applications based on PLCopen automata

Bibtex entry :

@inproceedings {  BSK16,
	author = { Bohlender, Dimitri and Simon, Hendrik and Kowalewski, Stefan },
	title = { Symbolic verification of PLC safety-applications based on
		PLCopen automata },
	booktitle = { MBMV 2016 : 19. GI/ITG/GMM-Workshop "Methoden und
		Beschreibungsprachen zur Modellierung und Verifikation von
		Schaltungen und Systemen" : Albert-Ludwigs-Universit{\"a}t
		Freiburg im Breisgau 1.–2. M{\"a}rz 2016 / Ralf Wimmer
		(Herausgeber) },
	publisher = { Albert-Ludwigs-Universit{\"a}t },
	pages = { 33-45 },
	year = { 2016 },
	address = { Freiburg im Breisgau },
	organization = { 19. GI/ITG/GMM-Workshop "Methoden und Beschreibungsprachen
		zur Modellierung und Verifikation von Schaltungen und
		Systemen", Freiburg im Breisgau (Germany), 2016-03-01 -
		2016-03-02 },
	doi = { 10.6094/UNIFR/10636 },
	typ = { PUB:(DE-HGF)7 },
	reportid = { RWTH-CONV-207902 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/573821/files/573821.pdf },
}

[BBJKNN14] PDFBIB

Bohlender, D., Bruintjes, H., Junges, S., Katelaan, J., Nguyen, V. Y., and Noll, T., "A Review of Statistical Model Checking Pitfalls on Real-Time Stochastic Models", in Proc. Leveraging Applications of Formal Methods, Verification and Validation. Specialized Techniques and Applications - 6th International Symposium, ISoLA 2014, Imperial, Corfu, Greece, October 8-11, 2014, Proceedings, Part {II}, 2014, IEEE, pp. 177-192.

A Review of Statistical Model Checking Pitfalls on Real-Time Stochastic Models

Bibtex entry :

@inproceedings { BBJKNN14,
	author = { Dimitri Bohlender and Harold Bruintjes and Sebastian Junges
		and Jens Katelaan and Viet Yen Nguyen and Thomas Noll },
	title = { A Review of Statistical Model Checking Pitfalls on Real-Time
		Stochastic Models },
	booktitle = { Leveraging Applications of Formal Methods, Verification and
		Validation. Specialized Techniques and Applications - 6th
		International Symposium, ISoLA 2014, Imperial, Corfu,
		Greece, October 8-11, 2014, Proceedings, Part {II} },
	pages = { 177--192 },
	publisher = { IEEE },
	publishedas = { Druck Online },
	isbn = { 978-3-662-45231-8 },
	language = { eng },
	year = { 2014 },
	timestamp = { Mon, 29 Sep 2014 11:09:02 +0200 },
	i11key = { conference },
	for_reporting_period = { 2014 },
}

[BBK13] PDF BIB

Biallas, S., Bohlender, D., and Kowalewski, S., "Boolean and Modular Abstractions for Programmable Logic Controllers", in Proc. Dependable Control of Discrete Systems : DCDS13. - Vol. 4, P. 1, Laxenburg, 2013, IFAC, pp. 97-102.

Boolean and Modular Abstractions for Programmable Logic Controllers

Bibtex entry :

@inproceedings {  BBK13,
	author = { Biallas, Sebastian and Bohlender, Dimitri and Kowalewski,
		Stefan },
	title = { Boolean and Modular Abstractions for Programmable Logic
		Controllers },
	booktitle = { Dependable Control of Discrete Systems : DCDS13. - Vol. 4,
		P. 1 },
	publisher = { IFAC },
	pages = { 97-102 },
	year = { 2013 },
	address = { Laxenburg },
	organization = { Dependable Control of Discrete Systems },
	doi = { 10.3182/20130904-3-UK-4041.00011 },
	typ = { PUB:(DE-HGF)8 },
	reportid = { RWTH-CONV-203363 },
	cin = { 120000 / 122810 },
	url = { http://publications.rwth-aachen.de/record/225788 },
}