Towards a denotational semantics of timed RSL using duration calculus

The Timed RAISE Specification Language(Timed RSL)is an extension of RAISE Specificatioin Language by adding time constructors for specifying real-time applications.Duration Calculus(DC) is a real-time interval logic,which can be used to specify and reason about timing and logical constraints on duration propoerties of Boolean states in a dynamic system.This paper gives a denotational semantics to a subset of Timed RSL expressions,using Duration Calculus extended with super-dense shop modality and notations to capture time point properties of piecewise continuous states of arbitrary types.Using this semantics,the paper pesents a proof rule for verifying Timed RSL iterative expressions and implements the rule to prove the satisfaction by a sample Timed RSL specification of its real-time requrements.     

时间区间时序逻辑的判定性与表达能力

模型检测技术在实时系统验证中被广泛使用。离散时间区间时序逻辑满足性是可判定的,因而也是可模型检测的。连续时间域时间区间时序逻辑是否可模型检测,则并不清楚。约束时间域到非负实数,证明了其可满足性是不可判定的,但存在该逻辑的可判定子集,并发现了这样的子集。由于模型检测问题可归约为时序逻辑满足性判定问题,因此结果表明,时间区间时序逻辑不可模型检测,但其可判定子集可模型检测。     

Model-checking discrete duration calculus

Duration Calculus was introduced in [ZHR91] as a logic to specify and reason about requirements for real-time systems. It is an extension of Interval Temporal Logic [Mos85] where one can reason about integrated constraints over time-dependent and Boolean valued states without explicit mention of absolute time. Several major case studies, e.g. the gas burner system in [RRH93], have shown that Duration Calculus provides a high level of abstraction for both expressing and reasoning about specifications. Using Timed Automata [A1D92] one can express how real-time systems can be constructed at a level of detail which is close to an actual implementation. We consider in the paper the correctness of Timed Automata with respect to Duration Calculus formulae. For a subset of Duration Calculus, we show that one can automatically verify whether a Timed Automaton ? is correct with respect to a formulaD, abbreviated ? ?D, i.e. one can domodel-checking. The subset we consider is expressive enough to formalize the requirements to the gas burner system given in [RRH93]; but only for a discrete time domain. Model-checking is done by reducing the correctness problem ? ?D to the inclusion problem of regular languages.     

Model-checking discrete duration calculus

Duration Calculus was introduced in [ZHR91] as a logic to specify and reason about requirements for real-time systems. It is an extension of Interval Temporal Logic [Mos85] where one can reason about integrated constraints over time-dependent and Boolean valued states without explicit mention of absolute time. Several major case studies, e.g. the gas burner system in [RRH93], have shown that Duration Calculus provides a high level of abstraction for both expressing and reasoning about specifications. Using Timed Automata [A1D92] one can express how real-time systems can be constructed at a level of detail which is close to an actual implementation. We consider in the paper the correctness of Timed Automata with respect to Duration Calculus formulae. For a subset of Duration Calculus, we show that one can automatically verify whether a Timed Automaton is correct with respect to a formulaD, abbreviated D, i.e. one can domodel-checking. The subset we consider is expressive enough to formalize the requirements to the gas burner system given in [RRH93]; but only for a discrete time domain. Model-checking is done by reducing the correctness problem D to the inclusion problem of regular languages.     

Checking Temporal Duration Properties of Timed Automata

In this paper, the problem of checking a timed automaton for a Duration Calculus formula of the form Temporal Duration Property is addressed. It is shown that Temporal Duration Properties are in the class of discretisable real-time properties of Timed Automata, and an algorithm is given to solve the problem based on linear programming techniques and the depth-first search method in the integral region graph of the automaton. The complexity of the algorithm is in the same class as that of the solution of the reachability problem of timed automata.     

A formal framework for modeling and validating Simulink diagrams

Simulink has been widely used in industry to model and simulate embedded systems. With the increasing usage of embedded systems in real-time safety-critical situations, Simulink becomes deficient to analyze (timing) requirements with high-level assurance. In this article, we apply Timed Interval Calculus (TIC), a real-time specification language, to complement Simulink with TIC formal verification capability. We elaborately construct TIC library functions to model Simulink library blocks which are used to compose Simulink diagrams. Next, Simulink diagrams are automatically transformed into TIC models which preserve functional and timing aspects. Important requirements such as timing bounded liveness can be precisely specified in TIC for whole diagrams or some components. Lastly, validation of TIC models can be rigorously conducted with a high degree of automation using a generic theorem prover. Our framework can enlarge the design space by representing environment properties to open systems, and handle complex diagrams as the analysis of continuous and discrete behavior is supported.     

使用延时演算的时间化RSL的指称语义

使用扩展的持续时间演算(EDC)模型,给出了时间化的RAISE描述语言(RSL)的一个子集的指称语义.在扩展的持续时间演算模型中加入了一些新的特征,并探究了它们的代数定律.这些定律在形式化实时程序和验证实时性质中起着重要作用.最后还给出了时间化RSL的一些代数定律.这些定律可以从其指称语义证明,并用于程序的转化和优化.     

Interactive Fuzzy Interval Reasoning for smart Web shopping

In this paper, we propose an Interactive Fuzzy Interval Reasoning (FIR) method by combining fuzzy logic with interval computing to better serve Web users in terms of effectiveness and flexibility. Web users may use convenient interval inputs for online shopping. In order to serve different customers based on their preferences, different personalized fuzzy partitions to meet different needs are provided for the different Web customers. The Interactive Fuzzy Interval Reasoning method is used to design the Web shopping agent. Java servlets and Microsoft Access are used to implement the fuzzy Web shopping system.     

带有时钟变量的线性时序逻辑与实时系统验证

为了描述实时系统的性质和行为,10多年来,各种不同的时序逻辑,如Timed Computation Tree Logic,Metric Interval Temporal Logic和Real-Time Temporal Logic等相继提出来.这些时序逻辑适于表示实时系统的性质和规范,但不适于表示实时系统的实现模型.这样,在基于时序逻辑的实时系统的研究中,系统的性质和实现通常是用两种不同的语言来表示的.定义了一个带有时钟变量的线性时序逻辑(linear temporal logic with clocks,简称LTLC).它是由Manna和Pnueli提出的线性时序逻辑在实时情况下的一个推广.LTLC既能表示实时系统的性质,又能很方便地表示实时系统的实现.它能在统一的语义框架中表示出从高级的需求规范到低级的实现模型之间的不同抽象层次上的系统描述,并且能用逻辑蕴涵来表示不同抽象层次的系统描述之间的语义一致性.LTLC的这个特点将有助于实时系统的性质验证和实时系统的逐步求精.     

物联网与感知矿山专题讲座之三——感知矿山物联网的特征与关键技术

指出了感知矿山物联网是在煤矿综合自动化基础上的延伸和扩展应用,因而,感知矿山物联网在很大程度上有别于综合自动化系统;由于煤矿应用的特点,感知矿山物联网与目前地面物联网应用也有一些不同之处;介绍了感知矿山物联网的特征,它主要表现在多系统综合应用、感知层开放、应用平台开放和适合构建逻辑子系统等几个方面;分析了感知层、网络层、应用层的关键技术和跨层的公共技术;给出了感知矿山物联网的开放性要求和标准建设。该文对更好地理解感知矿山物联网的建设具有一定的参考价值。     

Evaluating real-time software specification languages

In recent years, many notations and methods in real-time software engineering have been proposed. However, thorough experimentation to evaluate these notations and methods has not been carried out. This paper focuses on real-time software engineering specification languages: Unified Modeling Language (UML), Real-Time Object-Oriented Modeling Language (ROOM), Modecharts, statecharts, Mealy and Moore machines, finite state machines, classical logic, Z, ASTRAL, temporal logic, FNLOG, linear logic, Timed Communicating Sequential Processes (TCSP), Temporal Calculus of Communicating Systems (TCCS), ρ1, and Multilevel Specification. The basis for evaluating these software engineering specification languages is by using the Turing machines and Interaction machines. We classify them based on their computational capabilities.     

Interval Evaluations in the Analytic Hierarchy Process By Possibility Analysis

Since a pairwise comparison matrix in the Analytic Hierarchy Process (AHP) is based on human intuition, the given matrix will always include inconsistent elements violating the transitivity property. We propose the Interval AHP by which interval weights can be obtained. The widths of the estimated interval weights represent inconsistency in judging data. Since interval weights can be obtained from inconsistent data, the proposed Interval AHP is more appropriate to human judgment. Assuming crisp values in a pairwise comparison matrix, the interval comparisons including the given crisp comparisons can be obtained by applying the Linear Programming (LP) approach. Using an interval preference relation, the Interval AHP for crisp data can be extended to an approach for interval data allowing to express the uncertainty of human judgment in pairwise comparisons.     

Correctness criteria of some algorithms for uncertain reasoning using Incidence Calculus

Incidence Calculus is a technique for associating uncertainty values with logical sentences. These uncertainty values are called incidences and they are sets of points, which may be thought of as representing equivalence classes of situations, Tarskian models, or possible worlds. Incidence Calculus was originally introduced in [1]. Incidence Calculus was designed to overcome various inherent problems with purely numeric mechanisms for uncertain reasoning [2]. In particular, incidences can represent the dependence between sentences, which numbers cannot, and hence Incidence Calculus can provide genuine, probabilistic reasoning. In this paper we prove soundness and completeness results for some algorithms introduced in [1] and hence satisfy some of the correctness criteria for Incidence Calculus. These algorithms can be used for probabilistic reasoning and to check the consistency of the subjective probabilities of sentences.     

Probabilistic Situation Calculus

In this article we propose a Probabilistic Situation Calculus logical language to represent and reason with knowledge about dynamic worlds in which actions have uncertain effects. Uncertain effects are modeled by dividing an action into two subparts: a deterministic (agent produced) input and a probabilistic reaction (produced by nature). We assume that the probabilities of the reactions have known distributions.Our logical language is an extension to Situation Calculae in the style proposed by Raymond Reiter. There are three aspects to this work. First, we extend the language in order to accommodate the necessary distinctions (e.g., the separation of actions into inputs and reactions). Second, we develop the notion of Randomly Reactive Automata in order to specify the semantics of our Probabilistic Situation Calculus. Finally, we develop a reasoning system in MATHEMATICA capable of performing temporal projection in the Probabilistic Situation Calculus.     

Comparing model checking and logical reasoning for real-time systems

We apply both model checking and logical reasoning to a real-time protocol for mutual exclusion. To this end we employ PLC-Automata, an abstract notion of programs for real-time systems. A logic-based semantics in terms of Duration Calculus is used to verify the correctness of the protocol by logical reasoning. An alternative but consistent operational semantics in terms of Timed Automata is used to verify the correctness by model checkers. Since model checking of the full model does not terminate in all cases within an acceptable time we examine abstractions and their influence on model-checking performance. We present two abstraction methods that can be applied successfully for the protocol presented.Received June 1999Accepted in revised form September 2003 by M.R. Hansen and C. B. Jones     

Incidence calculus: A mechanism for probabilistic reasoning

Mechanisms for the automation of uncertainty are required for expert systems. Sometimes these mechanisms need to obey the properties of probabilistic reasoning. We argue that a purely numeric mechanism, like those proposed so far, cannot provide a probabilistic logic with truth functional connectives. We propose an alternative mechanism, Incidence Calculus, which is based on a representation of uncertainty using sets of points, which might represent situations models or possible worlds. Incidence Calculus does provide a probabilistic logic with truth functional connectives.     

Linguistic Applications of First Order Intuitionistic Linear Logic

In this paper we will discuss the first order multiplicative intuitionistic fragment of linear logic, MILL1, and its applications to linguistics. We give an embedding translation from formulas in the Lambek Calculus to formulas in MILL1 and show this translation is sound and complete. We then exploit the extra power of the first order fragment to give an account of a number of linguistic phenomena which have no satisfactory treatment in the Lambek Calculus. This revised version was published online in August 2006 with corrections to the Cover Date.     

基于PRET的编程模型

时间可预测性在信息物理系统设计领域正变得越来越重要,目前时间可预测性系统的设计分为编程模型和体系结构两个层次,编程模型的研究往往是基于传统RTOS而提出新的时间模型,体系结构层则是现有体系结构,设计的具有时间属性的指令集、流水线等等.基于时间可预测体系结构PRET和可预测时间模型LET的研究,提出将PRET和LET模型相结合的编程模型,并通过分析和实验证明了这种设计的可行性和优势,进一步证明了时间在系统设计中的重要性.     

Interval Duration Logic: Expressiveness and Decidability

We investigate a variant of dense-time Duration Calculus which permits model checking using timed/hybrid automata. We define a variant of the Duration Calculus, called Interval Duration Logic, (IDL), whose models are timed state sequences [1].A subset LIDL of IDL consisting only of located time constraints is presented. As our main result, we show that the models of an LIDL formula can be captured as timed state sequences accepted by an event-recording integrator automaton. A tool called IDLVALID for reducing LIDL formulae to integrator automata is briefly described. Finally, it is shown that LIDL has precisely the expressive power of event-recording integrator automata, and that a further subset LIDL- corresponds exactly to event-recording timed automata [2]. This gives us an automata-theoretic decision procedure for the satisfiability of LIDL– formulae.     

A proof system of the CaIT calculus

The Internet of Things (IoT) can realize the interconnection of people, machines, and things anytime, anywhere. Most of the existing research mainly focuses on the practical applications of IoT, and there is a lack of research on modeling and reasoning about IoT systems from the perspective of formal methods. Thus, the Calculus of the Internet of Things (CaIT) has been proposed to specify and analyze IoT systems before the actual implementation, which can effectively improve development efficiency, and enhance system quality and reliability. To verify the correctness of IoT systems described by CaIT, this paper presents a proof system for CaIT, in which specifications and verifications are based on the extended Hoare Logic with time. Furthermore, we explore the cooperation between isolated proofs to validate the postconditions of the communication actions occurring in these proofs, with a particular focus on broadcast communication. We also demonstrate the soundness of our proof system. A simple “smart home” is given to illustrate the availability of our proof system.