An Intelligent Assistant for Converting City Requirements to Formal Specification

TL;DR

This paper introduces CitySpec, an intelligent system that automatically converts human-written English city requirements into formal specifications, addressing language ambiguities and missing information in smart city monitoring systems.

Contribution

The paper presents CitySpec, a novel system that bridges language gaps and handles incomplete or ambiguous requirements for formal city specifications.

Findings

CitySpec effectively converts English requirements into formal specs.

It supports interactive completion and human-in-the-loop correction.

Online learning enhances CitySpec's adaptability.

Abstract

As more and more monitoring systems have been deployed to smart cities, there comes a higher demand for converting new human-specified requirements to machine-understandable formal specifications automatically. However, these human-specific requirements are often written in English and bring missing, inaccurate, or ambiguous information. In this paper, we present CitySpec, an intelligent assistant system for requirement specification in smart cities. CitySpec not only helps overcome the language differences brought by English requirements and formal specifications, but also offers solutions to those missing, inaccurate, or ambiguous information. The goal of this paper is to demonstrate how CitySpec works. Specifically, we present three demos: (1) interactive completion of requirements in CitySpec; (2) human-in-the-loop correction while CitySepc encounters exceptions; (3) online learning in CitySpec.