**排序方式：**共有11条查询结果，搜索用时 141 毫秒

1.

高安全级别可信数据库系统的自主访问控制机制设计中若干问题及其解决方法

**总被引：2，自引：0，他引：2**该文在分析TCES对DBMS的DAC机制的要求的基础上，分析了DBMS的DAC的策略机制，讨论了将DAC机制包含在TCB中的实现实例，重点分析了高安全级别可信DBMS的DAC设计中的关键问题并给出了几种实现高可靠性DAC的几种方法。 相似文献

2.

Lei Bu Xuandong Li 《International Journal on Software Tools for Technology Transfer (STTT)》2011,13(4):307-317

The existing techniques for reachability analysis of linear hybrid systems do not scale well to the problem size of practical
interest. The performance of existing techniques is even worse for reachability analysis of a composition of several linear
hybrid automata. In this paper, we present an efficient path-oriented approach to bounded reachability analysis of composed
systems modeled by linear hybrid automata with synchronization events. It is suitable for analyzing systems with many components
by selecting critical paths, while this task was quite insurmountable before because of the state explosion problem. This
group of paths will be transformed to a group of linear constraints, which can be solved by a linear programming solver efficiently.
This approach of symbolic execution of paths allows design engineers to check important paths, and accordingly increase the
faith in the correctness of the system. This approach is implemented into a prototype tool Bounded reAchability CHecker (BACH).
The experimental data show that both the path length and the number of participant automata in a system checked using BACH
can scale up greatly to satisfy practical requirements. 相似文献

3.

An MDE-based method for bridging different design notations

**总被引：1，自引：0，他引：1** Tian Zhang Frédéric Jouault Jean Bézivin Xuandong Li 《Innovations in Systems and Software Engineering》2008,4(3):203-213

Different communities have developed plenty of design notations for software engineering in support of practical (via UML)
and rigorous (via formal methods) approaches. Hence the problem of bridging these notations rises. Model-driven engineering
(MDE) is a new paradigm in software engineering, which treats models and model transformations as first class citizens. Furthermore,
it is seen as a promising method for bridging heterogeneous platforms. In this paper, we provide an MDE-based approach to
build bridges between informal, semi-formal and formal notations: Firstly, different notations are viewed as different domain
specification languages (DSLs) and introduced into MDE, especially into the ATLAS Model Management Architecture (AMMA) platform,
by metamodeling. Then, ATL transformation rules are built for semantics mapping. At last, TCS-based model-to-text syntax rules
are developed, allowing one to map models to programs. Consequently, different design notations in both graphical style and
grammatical style are bridged. A case study of bridging OMG SysML™ to LOTOS is also illustrated showing the validity and practicability
of our approach. 相似文献

4.

Most of the timed automaton model checking algorithms explore state spaces by enumeration of time zones. The data structure called Difference Bound Matrix (DBM) is widely adopted to represent time zones because of its efficiency and simplicity. In this paper, we first present a quadratic-time algorithm to compute the canonical form of the conjunction of a canonical DBM and a time guard or a location invariant. Based on this algorithm, we present a quadratic-time DBM-based successor algorithm for timed automaton model checking. 相似文献

5.

6.

李宣东 《计算机科学技术学报》2001,16(1):0-0

The paper proposes an approach to solving some verification problems of time petri nets using linear programming.The approach is based on the observation that for loop-closed time Ptri nets,it is only necessary to investigate a finite prefix of an untimed run of the underlying Petri net.Using the technique the paper gives solutions to reachabiltiy and bounded delay timing analysis problems.For both problems algorithms are given,that are decision procedures for loop-closed time Petri nets.and semi-decision procedures for general time Petri nets. 相似文献

7.

As discrete jumps and continuous flows tangle in the behavior of linear hybrid automata (LHA), the bounded model checking (BMC) for reachability of LHA is a challenging problem. Current works try to handle this problem by encoding all the discrete and continuous behaviors in the bound into a set of SMT formulas which can then be solved by SMT solvers. However, when the system size is large, the object SMT problem could be huge and difficult to solve. Instead of encoding everything into one constraint set, this paper proposes a SAT–LP–IIS joint-directed solution to conduct the BMC for reachability of LHA in a layered way. First, the bounded graph structure of LHA is encoded into a propositional formula set, and solved by SAT solvers to find potential paths which can reach the target location on the graph. Then, the feasibility of certain path is encoded into a set of linear constraints which can then be solved by linear programming (LP) efficiently. If the path is not feasible, irreducible infeasible set (IIS) technique is deployed to locate an infeasible path segment which will be fed to the SAT solver to accelerate the enumerating process. Experiments show that by this SAT–LP–IIS joint-directed solution, the memory usage of the BMC of LHA is well-controlled and the performance outperforms the state-of-the-art SMT-style competitors significantly. 相似文献

8.

Minxue Pan Xuandong Li 《International Journal on Software Tools for Technology Transfer (STTT)》2012,14(6):639-651

Message Sequence Chart (MSC) is a graphical and textual language for describing the interactions between system components, and MSC specifications (MSSs) are a combination of a set of basic MSCs (bMSCs) and a High-level MSC that describes potentially iterating and branching system behavior by specifying the compositions of basic MSCs, which offer an intuitive and visual way of specifying design requirements. With concurrent, timing, and asynchronous properties, MSSs are amenable to errors, and their analysis is important and difficult. This paper deals with timing analysis of MSC specifications with asynchronous concatenation. For an MSC specification, we require that for any loop, its first node be flexible in execution time and its any associated external timing constraint be enforced on the entire loop. Such an MSC specification is called a

*flexible loop-closed MSC specification*(FLMSS). We show that for FLMSSs, the*reachability analysis*and*bounded delay analysis*problems can be solved efficiently by linear programming. The solutions have been implemented into our tool TASS and evaluated by experiments. 相似文献9.

Component-based development allows one to build software from existing components and promises to improve software reuse and reduce costs. For critical applications, the user of a component must ensure that it fits the requirements of the application. To achieve this, testing is a well-suited means when the source code of the components is not available.

*Robustness testing*is a testing methodology to detect the vulnerabilities of a component under unexpected inputs or in a stressful environment. As components may fail differently in different states, we use a state machine based approach to robustness testing. First, a set of paths is generated to cover transitions of the state machine, and it is used by the test cases to bring the component into a specific control state. Second, method calls with invalid inputs are fed to the component in different states to test the robustness. By traversing the paths, the test cases cover more states and transitions compared to stateless API testing. We apply our approach to several components, including open source software, and compare our results with existing approaches. 相似文献10.

Xiaofeng Yu Yan Zhang Tian Zhang Linzhang Wang Jun Hu JianHua Zhao Xuandong Li 《Information Systems Frontiers》2007,9(4):391-409

The growing scale and complexity of the enterprise computing systems under distributed and heterogeneous environments present
new challenges to system development, integration, and maintenance. In this paper, we present a model driven Web service development
framework to combat these challenges. The framework capitalizes on the unified modeling language (UML) profile for enterprise
distributed object computing (EDOC), MDA (model-driven architecture) and Web services. Within the framework, firstly, a general
PIM (platform independent models) is created using the EDOC CCA structural specification and CCA choreography specification
which defines the general functions of a system. Secondly, the general PIM is broken down into sub-PIMs according to functional
decomposition, each of which can provide service independently and will be implemented in a Web service. Thirdly, all of the
PIMs are transformed to Web service interface models for publication and invoking. Afterward, transform each PIM to a BPEL
specified Web service orchestration model. Finally, supported by model transform techniques, the sub EDOC PIMs are implemented
into Web services on specific platforms. Automatic model transformation is the key to this framework, therefore, the transformation
from EDOC CCA models to WSDL specified Web service interface models and the transformation from EDOC CCA models to BPEL specified
Web service orchestration models are deeply discussed, and the detailed transformation rules are proposed. A case study is
also provided to demonstrate the effectiveness of these rules and the merits of this framework.

相似文献

Xuandong Li (Corresponding author)Email: |