Publication | Closed Access
AltaRica 3.0 assertions: The whys and wherefores
14
Citations
21
References
2017
Year
Artificial IntelligenceEngineeringReligious SymbolVerificationComputer-aided VerificationModel CheckingSoftware AnalysisFormal VerificationData IntegritySystems EngineeringFormal TechniqueFormal SpecificationFormal ModelingComputer EngineeringComputer ScienceAltarica 3.0Program AnalysisAutomated ReasoningFixpoint Assertion MechanismFormal Methods
In discrete event simulations, the system is assumed to change of state when and only when an event occurs. This change of state can be more or less sophisticated depending on the modeling formalism. In this article, we discuss the whys and wherefores of the fixpoint assertion mechanism introduced in AltaRica 3.0 to perform changes of states. We show how it can be used to handle complex phenomena such as change in flow directions depending on the states of components. We propose an efficient implementation of this mechanism, thanks to ideas stemmed in theoretical computer science and artificial intelligence. We compare the AltaRica 3.0 approach with alternative ones, including those of the previous versions of the language.
| Year | Citations | |
|---|---|---|
Page 1
Page 1