全文获取类型
收费全文 | 67篇 |
免费 | 3篇 |
专业分类
电工技术 | 1篇 |
化学工业 | 9篇 |
建筑科学 | 2篇 |
轻工业 | 1篇 |
无线电 | 3篇 |
一般工业技术 | 3篇 |
冶金工业 | 8篇 |
自动化技术 | 43篇 |
出版年
2023年 | 1篇 |
2022年 | 2篇 |
2021年 | 1篇 |
2018年 | 2篇 |
2017年 | 1篇 |
2016年 | 3篇 |
2014年 | 2篇 |
2013年 | 2篇 |
2012年 | 2篇 |
2011年 | 1篇 |
2010年 | 5篇 |
2009年 | 4篇 |
2008年 | 2篇 |
2007年 | 2篇 |
2006年 | 3篇 |
2005年 | 6篇 |
2004年 | 4篇 |
2003年 | 5篇 |
2002年 | 4篇 |
2001年 | 5篇 |
2000年 | 1篇 |
1997年 | 2篇 |
1995年 | 2篇 |
1993年 | 3篇 |
1988年 | 1篇 |
1986年 | 1篇 |
1984年 | 1篇 |
1978年 | 1篇 |
1969年 | 1篇 |
排序方式: 共有70条查询结果,搜索用时 15 毫秒
21.
Tissue engineering entails the in vitro or in vivo generation of replacement tissues from cells with the aid of supporting scaffolds and stimulating biomolecules, in order to provide biological substitutes for restoration and maintenance of human tissue functions. In this review, we summarize the main classes of degradable polymeric scaffolds, natural and synthetic ones, and the evolution made in this field from adaptation of materials in clinical use to the fabrication of “designer” scaffolds. 相似文献
22.
23.
Of special interest in formal verification are safety properties, which assert that the system always stays within some allowed region. Proof rules for the verification of safety properties have been developed in the proof-based approach to verification, making verification of safety properties simpler than verification of general properties. In this paper we consider model checking of safety properties. A computation that violates a general linear property reaches a bad cycle, which witnesses the violation of the property. Accordingly, current methods and tools for model checking of linear properties are based on a search for bad cycles. A symbolic implementation of such a search involves the calculation of a nested fixed-point expression over the system's state space, and is often infeasible. Every computation that violates a safety property has a finite prefix along which the property is violated. We use this fact in order to base model checking of safety properties on a search for finite bad prefixes. Such a search can be performed using a simple forward or backward symbolic reachability check. A naive methodology that is based on such a search involves a construction of an automaton (or a tableau) that is doubly exponential in the property. We present an analysis of safety properties that enables us to prevent the doubly-exponential blow up and to use the same automaton used for model checking of general properties, replacing the search for bad cycles by a search for bad prefixes. 相似文献
24.
Shoham Shamir Orna Kupferman Eli Shamir 《Electronic Notes in Theoretical Computer Science》2003,39(1):65-78
We study the distinguishing and expressive power of branching temporal logics with bounded nesting depth of path quantifiers. We define the fragments CTL*i and CTLi of CTL* and CTL, where at most i nestings of path quantifiers are allowed. We show that for all i ≥ 1, the logic CTL*i+1 has more distinguishing and expressive power than CTL*i; thus the branching-depth hierarchy is strict. We describe equivalence relations Hi that capture CTL*i: two states in a Kripke structure are Hi-equivalent iff they agree on exactly all CTL*i formulas. While H1 corresponds to trace equivalence, the limit of the sequence H1, H2,… is Milner's bisimulation. These results are not surprising, but they give rise to several interesting observations and problems. In particular, while CTL* and CTL have the same distinguishing power, this is not the case for CTL*i and CTLi. We define the branching depth of a structure as the minimal index i for which Hi+1=Hi. The branching depth indicates on the possibility of using bisimulation instead of trace equivalence (and similarly for simulation and trace containment). We show that the problem of finding the branching depth is PSPACE-complete. 相似文献
25.
Shoham Ben-David Orna Grumberg Tamir Heyman Assaf Schuster 《International Journal on Software Tools for Technology Transfer (STTT)》2003,4(4):496-504
This paper presents a scalable method for parallel symbolic on-the-fly model checking in a distributed memory environment. Our method combines a scheme for on-the-fly model checking for safety properties with a scheme for scalable reachability analysis. We suggest an efficient, BDD-based algorithm for a distributed construction of a counterexample. The extra memory requirement for counterexample generation is evenly distributed among the processes by a memory balancing procedure. At no point during computation does the memory of a single process contain all the data. This enhances scalability. Collaboration between the parallel processes during counterexample generation reduces memory utilization for the backward step. We implemented our method on a standard, loosely- connected environment of workstations, using a high-performance model checker. Our initial performance evaluation, carried out on several large circuits, shows that our method can check models that are too large to fit in the memory of a single node. Our on-the-fly approach may find counterexamples even when the model is too large to fit in the memory of the parallel system. 相似文献
26.
In this work we present a verification methodology for real-time distributed systems, based on their modular decomposition into processes. Given a distributed system, each of its components is reduced by abstracting away from details that are irrelevant for the required specification. The abstract components are then composed to form an abstract system to which a model checking procedure is applied. The abstraction relation and the specification language guarantee that if the abstract system satisfies a specification, then the original system satisfies it as well.The specification languageRTL is a branching-time version of the real-time temporal logicTPTL presented in Alur and Henzinger [1]. Its model checking is linear in the size of the system and exponential in the size of the formula. Two notions of abstraction for real-time systems are introduced, each preserving a sublanguage ofRTL. 相似文献
27.
Hana Chockler Orna Kupferman Moshe Vardi 《International Journal on Software Tools for Technology Transfer (STTT)》2006,8(4-5):373-386
In formal verification, we verify that a system is correct with respect to a specification. Even when the system is proven
to be correct, there is still a question of how complete the specification is and whether it really covers all the behaviors
of the system. The challenge of making the verification process as exhaustive as possible is even more crucial in simulation-based verification, where the infeasible task of checking all input sequences is replaced by checking a test suite consisting of
a finite subset of them. It is very important to measure the exhaustiveness of the test suite, and indeed there has been extensive
research in the simulation-based verification community on coverage metrics, which provide such a measure. It turns out that no single measure can be absolute, leading to the development of numerous
coverage metrics whose usage is determined by industrial verification methodologies. On the other hand, prior research of
coverage in formal verification has focused solely on state-based coverage. In this paper we adapt the work done on coverage
in simulation-based verification to the formal-verification setting in order to obtain new coverage metrics. Thus, for each
of the metrics used in simulation-based verification, we present a corresponding metric that is suitable for the setting of
formal verification and describe an algorithmic way to check it. 相似文献
28.
29.
In formal verification, we verify that a system is correct with respect to a specification. Even when the system is proved to be correct, there is still a question of how complete the specification is, and whether it really covers all the behaviors of the system. In this paper we study coverage metrics for model checking. Coverage metrics are based on modifications we apply to the system in order to check which parts of it were actually relevant for the verification process to succeed. We introduce two principles that we believe should be part of any coverage metric for model checking: a distinction between state-based and logic-based coverage, and a distinction between the system and its environment. We suggest several coverage metrics that apply these principles, and we describe two algorithms for finding the non-covered parts of the system under these definitions. The first algorithm is a symbolic implementation of a naive algorithm that model checks many variants of the original system. The second algorithm improves the naive algorithm by exploiting overlaps in the variants. We also suggest a few helpful outputs to the user, once the non-covered parts are found.
相似文献
Moshe Y. VardiEmail: |
30.
Selective Quantitative Analysis and Interval Model Checking: Verifying Different Facets of a System 总被引:1,自引:0,他引:1
In this work we propose a verification methodology consisting of selective quantitative timing analysis and interval model checking. Our methods can aid not only in determining if a system works correctly, but also in understanding how well the system works. The selective quantitative algorithms compute minimum and maximum delays over a selected subset of system executions. A linear-time temporal logic (LTL) formula is used to select either infinite paths or finite intervals over which the computation is performed. We show how tableau for LTL formulas can be used for selecting either paths or intervals and also for model checking formulas interpreted over paths or intervals.To demonstrate the usefulness of our methods we have verified a complex and realistic distributed real-time system. Our tool has been able to analyze the system and to compute the response time of the various components. Moreover, we have been able to identify inefficiencies that caused the response time to increase significantly (about 50%). After changing the design we not only verified that the response time was lower, but were also able to determine the causes for the poor performance of the original model using interval model checking. 相似文献