2006 · 11 citations · 6 references
ComputingComputer ScienceSystems EngineeringDistributed SystemsFormal MethodsSystems ArchitectureModel CheckingPetri NetsReliable Distributed SystemsReliable System DesignSystem MonitoringTiming SemanticsArchitecture MetamodelCommon InformationComponent-based ArchitecturesComputation Tree LogicComputational LogicComputational Tree LogicProbabilistic LogicRuntime Verification
It is now recognized that nonfunctional properties are important to practical software development and maintenance. Many of these properties involve time and probabilities - for example, reliability and availability. In this paper, we present a framework for runtime verification of timed and probabilistic nonfunctional properties of component-based architectures, built using the meta-object facility and the Distributed Management Task Force's common information model (CIM) standard. We describe a Microsoft .NET-based implementation of our framework. We use a language for contracts based on probabilistic computational tree logic (PCTL). We provide a formal semantics for this language based on possible application execution traces. The semantics is parametrized with respect to the choice of application states and state changes to be monitored. This enables us to use the language to define a wide range of nonfunctional properties. We explain how our framework associates constraints with systems that expose management information through the CIM, via a novel extension of the CIM metamodel.
6
A logic for reasoning about time and reliability
Hans Hansson, Bengt Jönsson · Formal Aspects of Computing · 1994 · 1.4K citations · Full text
PRISM 2.0: A Tool for Probabilistic Model Checking
2004 · 146 citations
PRISM 2.0: a tool for probabilistic model checking
Marta Kwiatkowska, Gethin Norman, David Parker · 2004 · 91 citations