Marjan Sirjani

Maghsood Salimi, Mohammad Loni, Sara Afshar et al.

The increasing demand for autonomous machines in construction environments necessitates the development of robust object detection algorithms that can perform effectively across various weather and environmental conditions. This paper introduces a new semantic segmentation dataset specifically tailored for construction sites, taking into account the diverse challenges posed by adverse weather and environmental conditions. The dataset is designed to enhance the training and evaluation of object detection models, fostering their adaptability and reliability in real-world construction applications. Our dataset comprises annotated images captured under a wide range of different weather conditions, including but not limited to sunny days, rainy periods, foggy atmospheres, and low-light situations. Additionally, environmental factors such as the existence of dirt/mud on the camera lens are integrated into the dataset through actual captures and synthetic generation to simulate the complex conditions prevalent in construction sites. We also generate synthetic images of the annotations including precise semantic segmentation masks for various objects commonly found in construction environments, such as wheel loader machines, personnel, cars, and structural elements. To demonstrate the dataset's utility, we evaluate state-of-the-art object detection algorithms on our proposed benchmark. The results highlight the dataset's success in adversarial training models across diverse conditions, showcasing its efficacy compared to existing datasets that lack such environmental variability.

Maryam Bagheri, Marjan Sirjani, Ehsan Khamespanah et al.

Autonomous traffic control systems are large-scale systems with critical goals. Due to the dynamic nature of the surrounding world of these systems, assuring the satisfaction of their properties at runtime and in the presence of a change is important. A prominent approach to assure the correct behavior of these systems is verification at runtime, which has strict time and memory limitations. To tackle these limitations, we propose Magnifier, an iterative, incremental, and compositional verification approach that operates on a component-based model. The Magnifier idea is zooming on the component affected by a change, verifying the correctness of properties of interest of the system after adapting the component to the change, and then zooming out and tracing the change if it propagates. If the change propagates, all components affected by the change are adapted and are composed to form a new component. Magnifier repeats the same process for the new component. This iterative process terminates whenever the propagation of the change stops. In Magnifier, we use the Coordinated Adaptive Actor model (CoodAA) of traffic control systems. We present a formal semantics for CoodAA as a network of Timed Input-Output Automata (TIOAs). The change does not propagate if TIOAs of the adapted component and its environment are compatible. We implement our approach in Ptolemy II. The results of our experiments indicate that the proposed approach improves the verification time and the memory consumption compared to a non-compositional approach.