{'fraction_non_alphanumeric': 0.023717948717948717, 'fraction_numerical': 0.019230769230769232, 'mean_word_length': 5.586497890295359, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Formalizing the Uni-processor Simplex Architecture

Simplex is a software architecture for dependable and evolvable process-control systems developed by the Software Engineering Institute. Our project consisted in creating a formal specification of this architecture, and analyzing its safety and liveness properties. We developed a CSP model to describe the overall dynamic behavior of the Simplex architecture, that we verified using the Failure-Divergence-Refinement (FDR) model checker. As a result, we discovered interesting things about the use of FDR that revealed subtle points in the Simplex architecture. We also developed a WRIGHT specification of this architecture to characterize precisely the connections between its components at the architectural evel. The specification was based on the latest version of the CSP model. The research reported here was sponsored in part by the Wright Laboratory, Aeronautical Systems Center, Air Force Materiel Command, USAF, and the Advanced Research Projects Agency (ARPA) under grants F33615-93-1-1330 and N66001-95-C8623; and by National Science Foundation Grant CCR-9357792. Views and conclusions contained in this document are those of the authors and should not be interpreted as representing the official policies, either expressed or implied, of Wright Laboratory, the US Department of Defense, the United States Government, or the National Science Foundation. The US Government is authorized to reproduce and distribute reprints for Government purposes, notwithstanding any copyright notation thereon.