Dimitri Bohlender, M.Sc. RWTH

Kontakt

Wissenschaftlicher Mitarbeiter

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


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

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

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

Publikationen


Publikations-Export
[BHK18]
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 = { 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 },
	url = { http://publications.rwth-aachen.de/record/752221 },
}
[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]
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 / edited by Carlo A. Furia, Kirsten Winter, 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 : 14th International Conference,
		IFM 2018, Maynooth, Ireland, September 5-7, 2018,
		Proceedings / edited by Carlo A. Furia, Kirsten Winter },
	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 },
	url = { http://publications.rwth-aachen.de/record/752219 },
}
[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 - Lehrstuhl Informatik 11 - Ahornstr. 55 - 52074 Aachen - Deutschland