Application development for the modern web involves sophisticated engineering workflows—including user interface (UI) aspects. Such user interfaces comprise web elements that are typically created with HTML/CSS markup and JavaScript-like languages, yielding web documents. Their testing entails performing checks to examine visual and structural parts of the resulting UI software against requirements such as usability, accessibility, performance, or, increasingly, compliance with standards. However, current techniques are largely ad hoc and tailor-made to specific classes of requirements or web technologies and extensively require human-in-the-loop qualitative evaluations. Web UI evaluation so far has lacked formal foundations, which would provide assurances of compliance with requirements in an automatic manner. To this end, we devise a methodology and accompanying technical framework for web UIs. In our approach, requirements are formally specified in a spatio-temporal logic able to capture both the layout of visual components as well as how they change over time, as a user interacts with them. The technique we advocate is independent of the underlying technologies a web application may be developed with, as well as the browser and operating system used. To concretely support the specification and evaluation of UI requirements, our framework is grounded on open source tools for instrumenting, analyzing, and reporting spatio-temporal behaviors in webpages. We demonstrate our approach in practice over web accessibility standards posing challenges for automated verification.

Application development for the modern Web involves sophisticated engineering workflows which include user interface aspects. Those involve Web elements typically created with HTML/CSS markup and JavaScript-like languages, yielding Web documents. WebMonitor leverages requirements formally specified in a logic able to capture both the layout of visual components as well as how they change over time, as a user interacts with them. Then, requirements are verified upon arbitrary web pages, allowing for automated support for a wide set of use cases in interaction testing and simulation. We position WebMonitor within a developer workflow, where in case of a negative result, a visual counterexample is returned. The monitoring framework we present follows a black-box approach, and as such is independent of the underlying technologies a Web application may be developed with, as well as the browser and operating system used.

From biological systems to cyber-physical systems, monitoring the behavior of such dynamical systems often requires reasoning about complex spatio-temporal properties of physical and computational entities that are dynamically interconnected and arranged in a particular spatial configuration. Spatio-Temporal Reach and Escape Logic (STREL) is a recent logic-based formal language designed to specify and reason about spatio-temporal properties. STREL considers each system's entity as a node of a dynamic weighted graph representing its spatial arrangement. Each node generates a set of mixed-analog signals describing the evolution over time of computational and physical quantities characterizing the node's behavior. While there are offline algorithms available for monitoring STREL specifications over logged simulation traces, here we investigate for the first time an online algorithm enabling the runtime verification during the system's execution or simulation. Our approach extends the original framework by considering imprecise signals and by enhancing the logics' semantics with the possibility to express partial guarantees about the conformance of the system's behavior with its specification. Finally, we demonstrate our approach in a real-world environmental monitoring case study.

Engineering cyber-physical systems inhabiting contemporary urban spatial environments demands software engineering facilities to support design and operation. Tools and approaches in civil engineering and architectural informatics produce artifacts that are geometrical or geographical representations describing physical spaces. The models we consider conform to the CityGML standard; although relying on international standards and accessible in machine-readable formats, such physical space descriptions often lack semantic information that can be used to support analyses. In our context, analysis as commonly understood in software engineering refers to reasoning on properties of an abstracted model-in this case a city design. We support model-based development, firstly by providing a way to derive analyzable models from CityGML descriptions, and secondly, we ensure that changes performed are propagated correctly. Essentially, a digital twin of a city is kept synchronized, in both directions, with the information from the actual city. Specifically, our formal programming technique and accompanying technical framework assure that relevant information added, or changes applied to the domain (resp. analyzable) model are reflected back in the analyzable (resp. domain) model automatically and coherently. The technique developed is rooted in the theory of bidirectional transformations, which guarantees that synchronization between models is consistent and well behaved. Produced models can bootstrap graph-theoretic, spatial or dynamic analyses. We demonstrate that bidirectional transformations can be achieved in practice on real city models.

Technological advances enable new kinds of smart environments exhibiting complex behaviors; smart cities are a notable example. Smart functionalities heavily depend on space and need to be aware of entities typically found in the spatial domain, e.g. roads, intersections or buildings in a smart city. We advocate a model-based development, where the model of physical space, coming from the architecture and civil engineering disciplines, is transformed into an analyzable model upon which smart functionalities can be embedded. Such models can then be formally analyzed to assess a composite system design. We focus on how a model of physical space specified in the CityGML standard language can be transformed into a model amenable to analysis and how the two models can be automatically kept in sync after possible changes. This approach is essential to guarantee safe model-driven development of composite systems inhabiting physical spaces. We showcase transformations of real CityGML models in the context of scenarios concerning both design time and runtime analysis of space-dependent systems.