“Designer” scaffolds for tissue engineering and regeneration

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.     

Model Checking of Safety Properties

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.     

Branching-Depth Hierarchies

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 CTL_i 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 H_i that capture CTL^*_i: two states in a Kripke structure are H_i-equivalent iff they agree on exactly all CTL^*_i formulas. While H₁ corresponds to trace equivalence, the limit of the sequence H₁, H₂,… 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 CTL_i. We define the branching depth of a structure as the minimal index i for which H_i+1=H_i. 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.     

Scalable distributed on-the-fly symbolic model checking

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.     

Modular abstractions for verifying real-time distributed systems

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.     

Coverage metrics for formal verification

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.     

以色列卡如也特 · 比利克绿色小学—如卡弗特学校校园设计

正在学年伊始、如卡弗特学校(Rakafot School)建设完工的2周后,作为这个学校的风景园林设计师,我们接到了一个意外的电话。"我想听听你们对于在学校‘冬日池塘’放养青蛙的意见。"来电话的是我们的农学老师,"我们听到了学生们对于蚊子的抱怨,因此我想,用青蛙来治理这些蚊子似乎是个不错的主意,而且青蛙的呱呱声伴随着孩子们的欢声笑语将会听起来很美妙。""这听起来     

Coverage metrics for temporal logic model checking*

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.

Selective Quantitative Analysis and Interval Model Checking: Verifying Different Facets of a System

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.