Monterey Phoenix (MP) is a formal language, approach, and tool for modeling mission, system and process behaviors. MP models and simulates behaviors of systems, software, hardware, people, organizations, and their dependencies on one another and the environment.  Models ranging from conceptual or mission level to detailed design level are supported. Many findings have been made at the architecture level of abstraction without modeling the implementation details.

The lightweight Formal Method employed by MP provides an ecosystem for sanity checking tools, reusable architecture patterns, reusable assertions, queries, and tools for extracting architecture views.  MP helps its users reason about intended behaviors, realize their own assumptions, turn assumptions into formal requirements, and expose and control certain types of emergent behaviors.  It supports modeling and simulation of system of systems (SoS) across many application domains.

MP was developed at the U.S. Navy Naval Postgraduate School (NPS) by Dr. Mikhail Auguston in the Department of Computer Sciences.  The concept of software behavior models based on event grammars and event traces was introduced in (Auguston 1991, 1995), (Auguston, Jeffery, & Underwood 2002), (Auguston, Michael, & Shing 2006) as an approach to software debugging and testing automation. The early drafts of Monterey Phoenix have appeared in (Auguston 2009 a, 2009 b, 2014), (Auguston, Whitcomb, & Giammarco 2010) and (Auguston & Whitcomb 2010, 2012).

MP has grown to support a variety of analyses including software safety analysis (Rivera 2011), business process modeling and analysis (Giammarco & Auguston 2013), (Giammarco et al 2014), (Auguston et al 2015), cost estimation (Farah-Stapleton & Auguston 2013), (Farah-Stapleton, Auguston & Giammarco 2016), (Farah-Stapleton 2016), model checking (Song 2015, 2016), scenario generation (Giammarco, Giles & Whitcomb 2017, Giammarco et al 2018), pattern detection (Quartuccio 2017, 2017a, 2020) and emergent behavior analysis (Giammarco & Auguston 2020).  New applications are ongoing in the areas of probabilistic modeling, cybersecurity, real-time systems analysis and risk analysis. See the Documentation page for a full bibliography, and the Import menu on MP-Firebird for example models.

Relevant capability.

Those working on complex systems with concerns of safety, cybersecurity, and/or mission-criticality want to know what latent unwanted behaviors are unintentionally being permitted by their design. Reliable, repeatable, and rapid generation of MP event traces is helping users expose unwanted behaviors in their missions, systems and processes. While other approaches and tools focus on helping users describe, communicate, and verify what they know, MP excels at helping users conceive of, communicate, validate, and control behaviors they hadn't previously noticed were possible.

Scope-complete.

MP fills a capability gap that is present in other behavior modeling approaches and languages used by the Navy: it generates the exhaustive set of event traces from a given behavior model up to a limited scope, and supports querying and checking of that set for the presence or absence of properties of interest.  Scope-complete sets of traces, loosed from constraints, often contain seeds of unwanted behaviors leading to realization of more latent assumptions critical for specifying good requirements.

The set of event traces produced by MP is guaranteed to be complete up to a scope limit decided by the user (maximum number of iterations).  The Small Scope Hypothesis states that most errors can be exposed on small examples.*  Many errors of consequence have been exposed using MP at a modest scope of 1, 2, or 3 iterations, demonstrating value from working with small scopes.

* Jackson, D. Software Abstractions: Logic, Language, and Analysis; MIT Press: Cambridge, MA, USA, 2012.

Workforce-accessible.

MP does not require its users to have expertise in formal methods to generate their own exhaustive sets of event traces more quickly and with less human error compared with manual methods.  Two available tools do trace generation for users while providing a gentle on-ramp to learning how to compose formal models and constraints at the user's own pace: MP-Firebird (https://firebird.nps.edu), which is web-based, and MP-Gryphon (https://nps.edu/mp/gryphon), which is locally installed. These two tools have slightly different feature sets, but similar interfaces to enables users to learn on one and then switch to the other as their needs dictate. Each has a text editor on the left, a graph display pane in the center, and a graph navigation pane on the right.

Intuitive graphs.

MP-Firebird and MP-Gryphon visualize event traces in a sequence diagram like format, with MP-Firebird having a swim lane option that resembles SysML activity diagrams.  Each separate actor’s behavior can be graphed as an activity diagram and global queries can be used to extract state diagrams and component diagrams from the same MP model, providing way to verify and validate MP specifications and also diagrams like those composed in Unified Modeling Language (UML), Systems Modeling Language (SysML), and Unified Architecture Framework (UAF).  Custom graphs can also be defined by the user to show dependencies of interest.

Support for queries and assertion checking.

As MP behavior models mature, querying is employed for testing for the presence or absence of model properties of interest.  A simple use of queries is to annotate traces containing event combinations of interest.  Other uses of queries include checking assertions about the presence or absence of a given property up to the scope the given model was run for (e.g.,  property X holds in every trace up to scope 3).

Event attributes to support quantitative reasoning.

MP supports computations for quantities associated with events such as time, risk, cost, power, and other quantitative resources. Events can be assigned probabilities of occurrence to support computation of conditional probabilities and whole trace probabilities. Reports, tables, and charts support the summary of properties of interest at both the local event trace level and the global (across all traces) level.  The advantage of basing quantitative analyses on MP event traces is that the analysis results are based on the scope-complete set of event traces rather than on a smaller subset of event traces (more possible behaviors are accounted for).

Simple event grammar.

MP consists of a simple event grammar with two basic relations: precedence (to establish event ordering) and inclusion (to establish event hierarchy).  From there, events are structured into alternative, optional and iterating branches to describe the behavior, similar to other executable modeling formalisms.   Unlike other formalisms, MP provides for the exhaustive generation, visualization, and querying of event traces from the event grammar rules and interaction constraints up to the specified scope.  This exhaustive set often contains seeds of unwanted behavior that can be discovered and weeded out of the design before they become entrenched in the implementation.