Modeling Software Behavior: A Craftsman's Approach

Issues in Behavior Modeling Views of Models Models of Software Traditional Goals Consistemcy Completeness Clarity Appropriate Goals Executability Provocation Processability Modeling Dichotomies Analysis/Synthesis Composition/Decomposition Prescribed/Proscribed Behavior Is/Does Fundamental Elements of Modeling Data Actions Events Threads Propositions Other Issues Size and Complexity Time Concurrency Math Background Graphs Degree of a Node Incidence Matrices Adjacency Matrices Connectedness Condensation Graphs Cyclomatic Number Directed Graphs Indegrees and Outdegrees Types of Nodes Adjacency Matrix of a Directed Graph Paths and Semipaths Reachability Matrix n-Connectedness Strong Components Model-Based Testing Examples Issues in Behavior Modeling Structured Programming Constructs Task Management Events Context-Sensitive Input Events Multiple-Context Output Events Discrete and Continuous Events Event Orders Continuing Examples Simplified U.S. 1040EZ Income Tax Form The NextDate Function Espresso Vending Machine Espresso Vending Machine (Full Version) Espresso Vending Machine (Six-Coin Version) Smart Fuel Pump Saturn Windshield Wiper Controller Examples for Readers Windchill Factor Table The Previous Date Function Saturn Cruise Control Programmable Thermostat Railroad Crossing Gate Controller The Pizza Robot Issues in the Examples Flowcharts Definition and Notation Technique Continuing Examples Simplified U.S. 1040EZ Income Tax Form The NextDate Function Espresso Vending Machine Smart Fuel Pump Saturn Windshield Wiper Controller Selected Examples for Readers Saturn Cruise Control The Pizza Robot Advantages and Limitations Decision Tables Definition and Notation Decision Table Analysis Decision Table Condensation Decision Tables with Mutually Exclusive Conditions Redundant and Inconsistent Decision Tables Continuing Examples Simplified U.S. 1040EZ Income Tax Form The NextDate Function First Try Second Try Third Try Espresso Vending Machine Smart Fuel Pump Saturn Windshield Wiper Controller Decision Table Engines Advantages and Limitations Finite State Machines Definition and Notation Technique Simplified U.S. 1040EZ Income Tax Form The NextDate Function Espresso Vending Machine Smart Fuel Pump Saturn Windshield Wiper Controller Finite State Machine Engines Advantages and Limitations Petri Nets Definition and Notation Transition Enabling and Firing Petri Net Conflict The Producer-Consumer Problem Technique Sequence, Selection, and Repetition Enable, Disable, and Activate Trigger Suspend, Resume, and Pause Conflict and Priority Mutual Exclusion Synchronization Some Consequences of Marking and Enabling Examples Simplified U.S. 1040EZ Income Tax Form The NextDate Function Espresso Vending Machine Smart Fuel Pump Saturn Windshield Wiper Controller Petri Net Engines Advantages and Limitations Event-Driven Petri Nets Definition and Notation Transition Enabling and Firing Context-Sensitive Input Events Multiple-Context Output Events Event Quiescence Examples Simplified U.S. 1040EZ Income Tax Form The NextDate Function Espresso Vending Machine Saturn Windshield Wiper Controller Event-Driven Petri Net Engines Advantages and Limitations Statecharts Definition and Notation Technique Examples Simplified U.S. 1040EZ Income Tax Form The NextDate Function Espresso Vending Machine Smart Fuel Pump Saturn Windshield Wiper Controller Statechart Engines Advantages and Limitations Object-Oriented Models Notation and Technique Use Case Diagrams Activity Diagrams State Machine Diagrams Sequence Diagrams Examples Simplified U.S. 1040EZ Income Tax Form The NextDate Function Espresso Vending Machine Smart Fuel Pump Saturn Windshield Wiper Controller Advantages and Limitations Model Comparisons Selecting an Appropriate Model Simplified U.S. 1040EZ Income Tax Form The NextDate Function Espresso Vending Machine Smart Fuel Pump Saturn Windshield Wiper Controller A Formal Consolidation of Executable Models Modus Ponens Casting a Decision Table into a Propositional Syllogism Casting a Finite State Machine into a Propositional Syllogism Casting an Event-Driven Petri Net into a Propositional Syllogism Casting a Statechart into a Propositional Syllogism Benefits of the Formalism Acknowledgment