Modeling an RCE Network Protocol with TLA+

Abstract

This work leverages the modeling language TLA+ to model the communication network of the software RCE. It begins by introducing the practical aspects of the TLA+ language to enable the development of a scalable model in TLA+ to verify errors that may arise through the interactions of asynchronous task executions. This work also presents an approach called the source mining approach, which is used to systematically analyze the program behavior implemented in Java based on predefined goals called modeling objectives. This approach collects all relevant system events related to relevant system variables, enabling the description of the behavior and the abstraction of specific aspects of the system during the asynchronous interaction of its components. This work further illustrates how a specification can be developed to be as simple as possible to shift the modeling effort toward verifying that changes in the system - caused by methods (also referred to as discrete events) - are safe and follow the logic of the intended behavior as defined by the model properties, rather than focusing on designing operator and specification logic. For this purpose, this RCE model incorporates a general approach and a generic operator that enables the consistent application of concurrent, thread-level methods to the system state and supports the extensibility of the model. The RCE model presented here also includes strategies that allow for the deterministic incorporation of the locations where behavior is observed in the implementation. The modeling approach and the model are demonstrated through analysis and modeling with the use case in which an RCE connection is established between two RCE instances. Within this scope, the work examines and highlights architecture components implemented in different services within the RCE network.