Dimitri Bohlender, M.Sc. RWTH

Contact

Research assistant

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


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

Address: Ahornstr. 55, 52074 Aachen, Germany

Office: Room 2302 (Building H, 3rd floor)


Open theses

At the moment no explicitly formulated, open topics are available. However if you are interested in formal methods, we can meet up and draft a suitable bachelor's or a master's thesis topic. Own suggestions are possible as well.

Teaching

Publications


Publikations-Export
[BHK18]
PDFBIB
Bohlender, D., Hamm, D., and Kowalewski, S., "Cycle-Bounded Model Checking of PLC Software via Dynamic Large-Block Encoding", in Proc. Proceedings of the 33rd Annual ACM Symposium on Applied Computing, 2018, ACM Press New York, New York, USA, 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 = { Proceedings of the 33rd Annual ACM Symposium on Applied
		Computing },
	publisher = { ACM Press New York, New York, USA },
	pages = { 1891-1898 },
	year = { 2018 },
	organization = { The 33rd 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 },
}
[BK18]
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 = { 14th IFAC International Workshop on Discrete Event Systems,
		Castellammare di Stabia (Italia), 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]
PDFBIB
Bohlender, D. and Kowalewski, S., "Design and Verification of Restart-Robust Industrial Control Software", in Proc. Integrated Formal Methods, Cham, 2018 in Lecture Notes in Computer Science, Springer International Publishing, 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 },
	publisher = { Springer International Publishing },
	pages = { 47-68 },
	series = { Lecture Notes in Computer Science },
	year = { 2018 },
	address = { Cham },
	organization = { 14th International Conference on integrated Formal Methods },
	doi = { 10.1007/978-3-319-98938-9_4 },
	typ = { PUB:(DE-HGF)7 },
	reportid = { RWTH-2018-231948 },
	cin = { 122810 / 120000 },
}
[UVS+18]
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], 2018 in IEEE International Conference on Emerging Technologies and Factory Automation-ETFA, IEEE, p. 4.

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

Bibtex entry :

@inproceedings {  UVS+18,
	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 },
	series = { IEEE International Conference on Emerging Technologies and
		Factory Automation-ETFA },
	year = { 2018 },
	address = { [Piscataway, NJ] },
	organization = { 22nd 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]
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 = { 13th 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]
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]
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]
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 },
	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 },
}

RWTH Aachen University - Chair of Computer Science 11 - Ahornstr. 55 - 52074 Aachen - Germany