Abstract
An Air Traffic Control System (ATCS) is a highly complex, real-time, and mission-critical system in software engineering, computer engineering, mathematical engineering, and design science. A general and rigorous methodology for complex system modeling and refinement via a closed loop of analysis-synthesis is presented in denotationalmathematics where the entire behaviors of a system are embodied as a synthesis of all analytic behaviors at the component level. The formal analysis-synthesis methodology is elaborated in a design paradigm of ATCS. An efficient denotational mathematics, Real-Time Process Algebra (RTPA), is adopted for modeling and refining the structures and functions of ATCS. In the analysis phase, the architectural models of ATCS are created and refined by a set of formal structure models (SMs), while the functional models of ATCS are specified and refined by a set of behavioral process models (PMs) at the component level. In the synthesis phase, the ATCS system is composed by the component PMs and SMs by process dispatching techniques. This work demonstrates that a highly complex ATCS system can be systematically and rigorously modeled, specified, and refined by RTPA and its methodology. As a result, the workload and complexity of large-scale software system modeling and development are efficiently reduced in software engineering. This work is presented in two papers in serial due to its excessive length. The behavioral process models of ATCS are described in this paper, which are based on the architectural models of ATCS as presented in JAMA 2(1).