Prof. Dr. Holger Schlingloff
Profil
Forschungsthemen8
AMVAD
Quelle ↗Förderer: Investitionsbank Berlin (IBB) Zeitraum: 01/2023 - 12/2025 Projektleitung: Prof. Dr. Holger Schlingloff, Prof. Dr. Lars Grunske
Big Data Analytics am Beispiel von Finanzdaten Preisgeld
Quelle ↗Zeitraum: 02/2014 - 12/2017 Projektleitung: Prof. Dr. Holger Schlingloff
CrESt: Modellbasierte Entwicklung kollaborativer eingebetteter Systeme
Quelle ↗Förderer: Bundesministerium für Forschung, Technologie und Raumfahrt Zeitraum: 02/2017 - 04/2020 Projektleitung: Prof. Dr. Holger Schlingloff
EXIST Gründungsstipendium: „Lexgraph“
Quelle ↗Förderer: BMWE: EXIST Zeitraum: 12/2025 - 11/2026 Projektleitung: Prof. Dr. Holger Schlingloff
Logische Analyse und formale Verifikation von offenen, interaktiven Multiagentensystemen
Quelle ↗Förderer: Bundesministerium für Forschung, Technologie und Raumfahrt Zeitraum: 06/2009 - 04/2012 Projektleitung: Prof. Dr. Holger Schlingloff
Prosafe
Quelle ↗Zeitraum: 03/2005 - 06/2006 Projektleitung: Prof. Dr. Holger Schlingloff
Research on Validation, Verification and Testing of Embedded Railway Applications
Quelle ↗Zeitraum: 01/2013 - 12/2014 Projektleitung: Prof. Dr. Holger Schlingloff
Stipendium für Herrn Mishra
Quelle ↗Zeitraum: 06/2004 - 05/2005 Projektleitung: Prof. Dr. Holger Schlingloff
Mögliche Industrie-Partner10
Stand: 26.4.2026, 19:48:44 (Top-K=20, Min-Cosine=0.4)
- 63 Treffer70.0%
- Workshop Reliable Methods and Mathematical ModelingP70.0%
- Workshop Reliable Methods and Mathematical Modeling
- 26 Treffer63.6%
- Engineering of New-Generation Protein Secretion SystemsP63.6%
- Engineering of New-Generation Protein Secretion Systems
- 26 Treffer63.6%
- Engineering of New-Generation Protein Secretion SystemsP63.6%
- Engineering of New-Generation Protein Secretion Systems
- 26 Treffer63.6%
- Engineering of New-Generation Protein Secretion SystemsP63.6%
- Engineering of New-Generation Protein Secretion Systems
- 10 Treffer61.8%
- Generalized Quatum Batalin-Vilkovisky Formalism and Graphical CalculusP61.8%
- Generalized Quatum Batalin-Vilkovisky Formalism and Graphical Calculus
- 10 Treffer61.8%
- Zuwendung im Rahmen des Programms „exist – Existenzgründungen aus der Wissenschaft“ aus dem Bundeshaushalt, Einzelplan 09, Kapitel 02, Titel 68607, Haushaltsjahr 2026, sowie aus Mitteln des Europäischen Strukturfonds (hier Euro-päischer Sozialfonds Plus – ESF Plus) Förderperiode 2021-2027 – Kofinanzierung für das Vorhaben: „exist Women“T61.8%
- Zuwendung im Rahmen des Programms „exist – Existenzgründungen aus der Wissenschaft“ aus dem Bundeshaushalt, Einzelplan 09, Kapitel 02, Titel 68607, Haushaltsjahr 2026, sowie aus Mitteln des Europäischen Strukturfonds (hier Euro-päischer Sozialfonds Plus – ESF Plus) Förderperiode 2021-2027 – Kofinanzierung für das Vorhaben: „exist Women“
Protatuans-Etaireia Ereynas Viotechologias Monoprosopi Etaireia Periorisments Eythinis
PT43 Treffer61.0%- Systematic Models for Biological Systems Engineering Training NetworkP61.0%
- Systematic Models for Biological Systems Engineering Training Network
- 43 Treffer61.0%
- Systematic Models for Biological Systems Engineering Training NetworkP61.0%
- Systematic Models for Biological Systems Engineering Training Network
- 44 Treffer61.0%
- Systematic Models for Biological Systems Engineering Training NetworkP61.0%
- Systematic Models for Biological Systems Engineering Training Network
- 43 Treffer61.0%
- Systematic Models for Biological Systems Engineering Training NetworkP61.0%
- Systematic Models for Biological Systems Engineering Training Network
Publikationen25
Top 25 nach Zitationen — Quelle: OpenAlex (BAAI/bge-m3 embedded für Matching).
Model Checking
19994257 Zitationen
Model Checking
2001Elsevier eBooks · 383 Zitationen · DOI
Formal Methods in System Design · 92 Zitationen · DOI
Autonomous Agents and Multi-Agent Systems · 76 Zitationen · DOI
Abstract A computational system is called autonomous if it is able to make its own decisions, or take its own actions, without human supervision or control. The capability and spread of such systems have reached the point where they are beginning to touch much of everyday life. However, regulators grapple with how to deal with autonomous systems, for example how could we certify an Unmanned Aerial System for autonomous use in civilian airspace? We here analyse what is needed in order to provide verified reliable behaviour of an autonomous system, analyse what can be done as the state-of-the-art in automated verification, and propose a roadmap towards developing regulatory guidelines, including articulating challenges to researchers, to engineers, and to regulators. Case studies in seven distinct domains illustrate the article.
Electronic Notes in Theoretical Computer Science · 71 Zitationen · DOI
We give an overview on web services and the web service technology stack. We then show how to build Petri net models of web services formulated in the specification language BPEL4WS. We define an abstract correctness criterion for these models and study the automated verification according to this criterion. Finally, we relate correctness of web service models to the model checking problem for alternating temporal logics.
39 Zitationen · DOI
We investigate expressivity and complexity of hybrid logics on linear structures. Hybrid logics are an enrichment of modal logics with certain first-order features which are algorithmically well behaved. Therefore, they are well suited for the specification of certain properties of computational systems. We show that hybrid logics are more expressive than usual modal and temporal logics on linear structures, and exhibit a hierarchy of hybrid languages. We determine the complexities of the satisfiability problem for these languages and define an existential fragment of hybrid logic for which satisfiability is still NP-complete. Finally, we examine the linear time model checking problem for hybrid logics and its complexity.
Journal of Applied Non-Classical Logics · 31 Zitationen · DOI
ABSTRACT Many temporal and modal logic languages can be regarded as subsets of first order logic, i.e. the semantics of a temporal logic formula is given as a first order condition on points of the underlying models (Kripke structures). Often the set of possible models is restricted to models which are trees. A temporal logic language is (first order) expressively complete, if for every first order condition for a node of a tree there exists an equivalent temporal formula which expresses the same condition. In this paper expressive completeness of the temporal logic language with the set of operators U (until), S (since), and X k (k-next) is proved, and the result is extended to various other tree-like structures.
Lecture notes in computer science · 28 Zitationen · DOI
Lecture notes in computer science · 28 Zitationen · DOI
25 Zitationen · DOI
In this paper, we deal with coverage criteria for boundary testing. We focus on the automatic generation of boundary tests based on OCL expressions and evaluate the quality of these tests with established coverage criteria like MC/DC. We define and apply new coverage criteria, evaluate their efficiency via mutation testing, and substantiate all explanations by an example, part of a model of an elevator control.
Lecture notes in computer science · 19 Zitationen · DOI
Texts in theoretical computer science · 17 Zitationen · DOI
17 Zitationen · DOI
In this paper, we develop a testing theory for specification-based software product line development. Starting with a framework for the evaluation of test cases with respect to formal specifications, we develop a notion of enhancement, which allows to re-use test cases in a horizontal systems development process. In such a process, more and more features are added to an existing software product. For specification-based testing, this means that the corresponding specifications are enhanced more and more, and that new test cases must be added to an existing test suite in order to test the additional features. We formally define an enhancement relation between Csp-CASL specifications, describe a test evaluation method for software product lines based on Csp-CASL specifications, and prove several preservation results which allow to re-use test cases in a horizontal development. We illustrate our approach with the example of a product line of remote control units for consumer products.
Lecture notes in computer science · 16 Zitationen · DOI
Computational analysis, synthesis, and design of dynamic models series · 16 Zitationen · DOI
S.77-110
Lecture notes in computer science · 16 Zitationen · DOI
Reliability Engineering & System Safety · 14 Zitationen · DOI
Automatic train control systems are complex and software-intensive cyber–physical systems. Hazard prediction at runtime for such systems has emerged as an essential research topic. Since hazards in train operations have a wide range of causal factors, the current monitoring approaches based on pre-programmed safety properties are generally ineffective in guaranteeing system safety. This paper proposes a reachable set-based runtime verification approach. In this approach, top-level train operation hazards are predicted directly by analysing all possible time-position states of the train from an observation. First, the train operation model is formalised with the parametric hybrid automata (PHA) to capture the discrete-continuous mixed and multi-variant features of train operations. Then, a model refinement algorithm is proposed based on an over-approximation linearisation method to reduce the computational complexity. The reachable set of the refined model is computed with the well-developed tool SpaceEx. We prove that this approximation approach does not compromise the hazard prediction ability. Furthermore, with a concrete example of the Beijing Yizhuang metro line, we analyse the feasibility of the approach in practice. The results indicate that the approach has high performance and accuracy for predicting train operation hazards and improves the safety of train operations.
14 Zitationen · DOI
A collaborative embedded systems (CES) is an intelligent agent in a cyber-physical system which cooperates with others by negotiation to fulfill a common task. In this paper, we consider autonomous transport robots as CES. These robots are used in production environments like factories and storage halls to realize the flow of materials within the production process. We describe the software hierarchy of the agents with self-localization, route planning and job scheduling. Then we discuss implementation strategies and possible benefits of a collaborative approach. Finally, we report on our modeling of the system for simulation and verification.
14 Zitationen · DOI
Testing is one of the most important quality assurance techniques for software. Automating the test design allows for automatically creating test suites from high-level system descriptions or test descriptions. Furthermore, it enables testers to automatically adapt the test suites to potentially recently changed descriptions. In model-based testing, models are used to automatically create test cases. Case studies report of an effort reduction in test design between 20 and 85 percent. In this paper, we report on a pilot project for introducing model-based testing in an industrial context. For such a pilot project, it is necessary to adapt the existing workflows and tool chains, to train the staff, and to adapt the assets of the company. The goal is to show the full applicability of the technique at the customer site. We present the evaluations, the lessons learned, and compare the efforts of model-based and manual test design for this example. This paper is not 'generally valid' in the sense that the results are reproducible for other projects and domains. Instead, our intention is to provide guidance for setting up similar evaluations.
14 Zitationen
Abstract. In this paper, we present a rewriting based monitoring algorithm for time propositional temporal logic (TPTL), which is a classic time extension of linear temporal logic (LTL). TPTL has been shown to be more expressive than other real-time extensions of LTL, e.g., metric temporal logic (MTL). We first describe the syntax and semantics of TPTL on finite time-traces. Using Maude, which is an executable environment for various logics, we give rewriting clauses to check whether a finite time-trace satisfies a TPTL formula. We use our algorithm to test a concrete example from the European Train Control System (ETCS), and evaluate it on several benchmarks. The results show the feasibility of our approach. 1
Systems Engineering · 12 Zitationen · DOI
ABSTRACT Digital twins are increasingly used across a wide range of industries. Modeling is a key to digital twin development—both when considering the models which a digital twin maintains of its real‐world complement (“models in digital twin”) and when considering models of the digital twin as a complex (software) system itself. Thus, systematic development and maintenance of these models is a key factor in effective and efficient digital twin development, maintenance, and use. We argue that model‐driven engineering (MDE), a field with almost three decades of research, will be essential for improving the efficiency and reliability of future digital twin development. To do so, we present an overview of the digital twin life cycle, identifying the different types of models that should be used and re‐used at different life cycle stages (including systems engineering models of the actual system, domain‐specific simulation models, models of data processing pipelines, etc.). We highlight some approaches in MDE that can help create and manage these models and present a roadmap for research towards MDE of digital twins.
Lecture notes in computer science · 12 Zitationen · DOI
12 Zitationen · DOI
In this paper, we present a theory for the evaluation of test cases with respect to formal specifications. In particular, we use the specification language CSP-CASL to define and evaluate black-box tests for reactive systems. Using loose semantics and three-valued test oracles, our approach is well-suited to deal with the refinement of specifications. In a structured development process of computational systems, abstract specifications are gradually refined into more concrete ones. With our approach, it is possible to develop test cases already from very abstract and basic specifications, and to reuse them later on in more refined systems.
11 Zitationen · DOI
A collaborative embedded system is an intelligent agent in a cyber-physical system which cooperates with others by negotiation to fulfill individual and common goals. Examples are self-driving cars, soccer-playing robots, or adaptive production plants. In this contribution, we present the industrial case study of autonomous transport robots in factory environments. In our setting, the robots collaborate by competing for transport jobs issued by the production machines. Each robot calculates its individual cost incurring with the job (in terms of distance, time, energy, wear and tear, etc.) and places a bid based on this cost. Then a distributed voting takes place, where the lowest cost bid wins the job. Here, we present our results of specifying and verifying this scenario. We collected requirements via user stories for the scenario, formulated these in suitable specification languages, designed executable models as simulation environments, and used statistical model checking and runtime monitoring for analysing the scenario. We argue that for different aspects of the case study, different analysis methods are to be used. However, all of these methods can make use of the fact that the goals of the individual agents coincide. Our results indicate that by the individual optimization of the cost function, reliability and performance of the collaborative group increases. We believe that this result is typical for a large number of similar systems.
10 Zitationen · DOI
The six-minute walking test (6MWT) is an essential test for evaluating exercise tolerance in many respiratory and cardiovascular diseases. Frailty and sarcopenia can cause rapid aging of the cardiovascular system in elderly people. Early detection and evaluation of frailty and sarcopenia are crucial for determining the treatment method. We aimed to develop a wearable measuring system for the 6MWT and propose a method for identifying frailty and quantifying walking muscle strength (WMS). In this study, 60 elderly participants were asked to wear accelerometers behind their left and right ankles during the 6MWT. The gait data were collected by a computer or smartphone. We proposed a method for analyzing walking performance using the stride length (SL) and step cadence (SC) instead of gait speed directly. Four regions (Range I-IV) were divided by cutoff values of SC = 2.0 [step/s] and SL = 0.6 [m/step] for a quick view of the frail state. There were 62.5% of frail individuals distributed in Range III and 72.4% of non-frail individuals in Range I. A concept of a WMS score was proposed for estimating WMS quantitatively. We found that 62.5% of frail individuals were scored as WMS1 and 41.4% of the non-frail elderly as WMS4. The average walking distances corresponding to WMS1-4 were 207 m, 370 m, 432 m, and 462 m, respectively. The WMS score may be a useful tool for quantitatively estimating sarcopenia or frailty due to reduced cardiopulmonary function.
Kooperationen0
Bestätigte Forscher↔Partner-Paare aus HU-FIS — Gold-Standard-Positive für das Matching.
Aus HU-FIS sind keine Kooperationen für diese Person gemeldet.
Stammdaten
Identität, Organisation und Kontakt aus HU-FIS.
- Name
- Prof. Dr. Holger Schlingloff
- Titel
- Prof. Dr.
- Fakultät
- Mathematisch-Naturwissenschaftliche Fakultät
- Institut
- Institut für Informatik
- Arbeitsgruppe
- Softwaretechnik (S)
- Telefon
- +49 30 2093-41190
- HU-FIS-Profil
- Quelle ↗
- Zuletzt gescrapt
- 26.4.2026, 01:11:53