1994 · 34 citations · 0 references
ComputingComputer ScienceInformation SystemsFormal MethodsKnowledge RepresentationSystems ArchitectureDeductive VerificationModel CheckingTelephone OperationsTemporal Knowledge RepresentationTemporal LogicTemporal OrderingModular Design SpecificationTemporal Logic AssertionsTemporal Logic ReasoningTemporal Logic SpecificationTemporal Logic VerificationTemporal OperatorsTemporal Specifications
. We outline a methodology for the modular specification of telephone services within first-order linear-time temporal logic. Typically, the services offered by a telephone system consist of a basic service and several optional additional services, such as automatic callback, redirection, etc. We argue informally that temporal logic provides a flexible formalism for the specification of individual services, and for the composition of different services. We present a style of specification, in which the expected behavior of each additional service can be specified independently of other services. In this style, it is straight-forward to compose noninteracting services. We outline, by means of examples, how certain interactions between services that prescribe conflicting behavior can manifest themselves as inconsistencies when the services are composed. We then outline how the resolution of such interactions can be described in the formalism. 1 Introduction The difficulty of designing ...