Search

Upscaling motor protein activity to perform work in man-made devices has long been an ambitious goal in bio-nanotechnology. The use of hierarchical motor assemblies, as realized in sarcomeres, has so far been complicated by the challenges of arranging sufficiently high numbers of motor proteins with nanoscopic precision. Here we suggest an alternative approach based on actomyosin cortex-like force production, allowing low complexity motor arrangements in a contractile meshwork that can be locally activated by ATP. The design is reminiscent of a motorized exoskeleton coating and thereby actuating soft protein-based polymer structures from the outside. This readily supports the connection and assembly of micro-3D printed modules into larger structures, thereby scaling up mechanical work. We provide an analytical model of force production in these systems and demonstrate the design flexibility by 3D printed units performing complex mechanical tasks, such as micro-arms and hands that perform sign language and wave.

Point-of-care testing (POCT) in low-resource settings requires tools that can operate independent of typical laboratory infrastructure. Due to its favorable signal-to-background ratio, a wide variety of biomedical tests utilize fluorescence as a readout. However, fluorescence techniques often require expensive or complex instrumentation and can be difficult to adapt for POCT. To address this issue, we developed a pocket-sized fluorescence detector costing less than $15 that is easy to manufacture and can operate in low-resource settings. It is built from standard electronic components, including an LED and a light dependent resistor, filter foils and 3D printed parts, and reliably detected less than 10 nM fluorescein concentrations (with a lower limit of detection of ≈6.8 nM), which is sufficient to follow typical biochemical reactions used in POCT applications. All assays are conducted on filter paper, which allows for a flat detector architecture to improve signal collection. We validate the device by quantifying in vitro RNA transcription and also demonstrate sequence-specific detection of target RNAs in the nanomolar range using a Cas13a-based fluorescence assay. Cas13a is a RNA-guided, RNA-targeting CRISPR effector with promiscuous RNase activity upon recognition of its RNA target. Cas13a sensing is highly specific and adaptable and in combination with our detector represents a promising approach for nucleic acid POCT. Furthermore, our open-source device architecture could be a valuable educational tool that integrates hardware, software and biochemistry concepts.

As autonomous vehicles, or AVs, enter the market, other road users will need to interact with them in an effective manner. Currently, in manuallydriven cars, the effectiveness of this interaction is based on the rules of the road that define priorities as well as ad-hoc negotiations to resolve conflicts. To formalize the conflict issue, we introduce the concept of legal zones showing how the road space can be described as graph of these zones. We also introduce the concept of operational regions around a vehicle which must not be infringed upon by others (to avoid safety conflicts). Using these two concepts we show how it is possible to consider new rules for the management of conflict in AV operations. We first briefly describe a new protocol for lane changes and then focus our attention on a protocol for managing conflicts in a pedestrian crossing situation.

Objective: We present a formal approach and methodology for the analysis and generation of user interfaces, with special emphasis on human-automation interaction. Background: A conceptual approach for modeling, analyzing, and verifying the information content of user interfaces is discussed. Methods: The proposed methodology is based on two criteria: First, the interface must be correct — that is, given the interface indications and all related information (user manuals, training material, etc.), the user must be able to successfully perform the specified tasks. Second, the interface and related information must be succinct — that is, the amount of information (mode indications, mode buttons, parameter settings, etc.) presented to the user must be reduced (abstracted) to the minimum necessary. Results: A step-by-step procedure for generating the information content of the interface that is both correct and succinct is presented and then explained and illustrated via two examples. Conclusions: Every user interface is an abstract description of the underlying system. The correspondence between the abstracted information presented to the user and the underlying behavior of a given machine can be analyzed and addressed formally. Applications: The procedure for generating the information content of user interfaces can be automated, and a software tool for its implementation has been developed. Potential application areas include adaptive interface systems and customized/personalized interfaces.

In this paper we discuss a formal approach and methodology for reducing and Abstracting the internal states and transitions of a (discrete-event) system representation. The resulting Abstracted description, called the “user model,” forms the foundation of the user interface as it formulates the necessary modes, states and transitions that drive the interface.

Alan Turing, in “The Chemical Basis of Morphogenesis” [Turing AM (1952) Philos Trans R Soc Lond 237(641):37–72], described how, in circular arrays of identical biological cells, diffusion can interact with chemical reactions to generate up to six periodic spatiotemporal chemical structures. Turing proposed that one of these structures, a stationary pattern with a chemically determined wavelength, is responsible for differentiation. We quantitatively test Turing’s ideas in a cellular chemical system consisting of an emulsion of aqueous droplets containing the Belousov–Zhabotinsky oscillatory chemical reactants, dispersed in oil, and demonstrate that reaction-diffusion processes lead to chemical differentiation, which drives physical morphogenesis in chemical cells. We observe five of the six structures predicted by Turing. In 2D hexagonal arrays, a seventh structure emerges, incompatible with Turing’s original model, which we explain by modifying the theory to include heterogeneity.

Nondeterminism in discrete-event systems occurs in many practical situations and often as a result of partial observability of events. For the adequate description of nondeterministic systems and nondeterministic phenomena, the trajectory-model formalism was introduced by Heymann (1991) and Heymann et al. (1991). This formalism has been used in by Shayman et al. (1995) for obtaining various results on supervisory control of nondeterministic systems subject to language specifications. In the present paper we develop a theory of supervisory control for nondeterministic discrete-event systems subject to both language and trajectory-model specifications. We further show how well-known algorithms for supervisory control (of deterministic systems) under partial observation can be adapted for synthesis of supervisors for nondeterministic systems subject to both language and trajectory-model specifications.

There have been rapid advances in control and automated driving aids in today's cars, with a concomitant rise in the breadth and complexity of driver interaction. Thus there is a need for a clear, consistent, logical, and holistic design methodology to the design and analysis of the driver-vehicle interaction environment. Such design method should also take into account expected future technological enhancements and advances. In this paper we present some emerging automated driving aids that are currently implemented in modern vehicles and those that are anticipated in the coming years. We focus on three automation features -- adaptive cruise control (ACC), Lane Centering (LC), and Full Speed Range ACC (FSRA). The design methodology is based on formal modeling of the functionality and user interaction of these systems and analysis of their corresponding user interfaces. The approach demonstrated here is valid for a wide range of user interaction systems where operational complexity requires careful and verifiable design.

We describe a formal, model-based, approach for the analysis and design of human-automation interaction. The approach is guided by two primary objectives: first, that the interaction be correct in the sense that it will enable the user to operate the system reliably; second, that the interaction be as simple as possible while maintaining all the required operational flexibility. With these objectives we first discuss a methodology for verification of user-interface correctness, thereby addressing the issue of operational reliability, and then present an algorithmic approach for designing simple and succinct interfaces.

In this paper we discuss a formal approach to the design and analysis of automotive systems, from a human-machine interaction (HMI) point of view. Specifically, we detail the behavior of a generic climate control system, present a statecharts model of this system, and discuss aspects of user interaction analysis. Several general principles for the design of climate control systems are illustrated and discussed. The topic of design patterns, in the context of a formal description of user interaction, is introduced, and two design patterns are illustrated and discussed.

Much of discrete event control theory has been developed within the framework of automata and formal languages. An alternative approach inspired by the theories of process-algebra as developed in the computer science literature is presented. The framework, which rests on a new formalism of concurrency, can adequately handle nondeterminism and can be used for analysis of a wide range of discrete event phenomena. >

A discrete-event process is modeled as a controlled state machine, in the framework of D.J. Ramadge and W.M. Wohman (1986). Their approach is extended to model a class of real-time discrete-event processes by means of a special type of automaton, called a clock automaton. The clock automaton is used for decreasing the real-time behavior of processes, controllers, and real-time specifications. >

Nondeterminism in discrete-event systems may occur as a result of partial modeling. For the adequate description of nondeterministic systems and nondeterministic phenomena, Heyman's trajectory-model formalism (1990, 1991) is employed. In the present paper we develop a theory of supervisory control for nondeterministic discrete-event systems subject to trajectory-model specifications. We show how well known algorithms for supervisory control (of deterministic systems) under partial observation can be adapted for synthesis of supervisors for nondeterministic systems.

The authors examine a class of discrete event systems (DESs) modeled as asynchronous hierarchical state machines (AHSMs). For this class of DESs, they provide an efficient method for testing reachability, which is an essential step in many control synthesis procedures. This method utilizes the asynchronous nature and hierarchical structure of AHSMs, thereby illustrating the advantage of the AHSM representation as compared with its equivalent (flat) state machine representation. An application of the method is presented where an online minimally restrictive solution is proposed for the problem of maintaining a controlled AHSM within prescribed legal bounds. >

Extends the formalism of prioritized synchronous composition (PSC), proposed by Heymann for modeling interaction (and control) of discrete event systems, to permit system interaction with their environment via interface masks. This leads to the notion of masked prioritized synchronous composition (MPSC), which we formally define, MPSC can be used to model interaction of systems at single as well as multiple interfaces. We show that MPSC can alternatively be computed by "unmasking" the PSC of "masked" systems, thereby establishing a link between MPSC and PSC. We next prove that MPSC is associative and thus suitable for modeling and analysis of supervisory control of discrete event systems. Finally, we use MPSC of a discrete event plant and a supervisor for controlling the plant behavior and show (constructively) that under the absence of "driven" events, controllability together with normality of the given specification serve as conditions for the existence of a supervisor. This extends the results on supervisory control, which permits control and observation masks to be associated with the plant only.

This paper discusses a formal and rigorous approach to the analysis of operator interaction with machines. It addresses the acute problem of detecting design errors in human-machine interaction and focuses on verifying the correctness of the interaction in complex and automated control systems. The paper describes a systematic methodology for evaluating whether the interface provides the necessary information about the machine to enable the operator to perform a specified task successfully and unambiguously. It also addresses the adequacy of information provided to the user via training material (e.g., user manual) about the machine's behavior. The essentials of the methodology, which can be automated and applied to the verification of large systems, are illustrated by several examples and through a case study of pilot interaction with an autopilot aboard a modern commercial aircraft. The expected application of this methodology is an augmentation and enhancement, by formal verification, of human-automation interfaces.

In this paper we address the problem of designing systems for human-automation interaction that insure satisfaction of a wide range of performance requirements (such as guaranteeing the safety and liveness of mission critical operations). Our approach is based on formal procedures that focus on the information provided to the user. We propose a formal methodology for constructing interfaces and corresponding user- manuals that is based on performing a systematic abstraction of the behavioral model of the system. The procedure is aimed at achieving two objectives: First, the interface must be correct in that with the given interface the user will be able to perform the specified tasks correctly. Secondly, the interface must be succinct. The paper discusses the underlying concepts and the formal methods for this approach. Two examples are used to illustrate the methodology. The algorithm for constructing interfaces that is proposed in the paper can be automated, and a preliminary software system for its implementation has been developed.

Liveness in hybrid systems is defined as the ability of the system to complete a specified task under all operating conditions and for all possible runs. Liveness is classified in the present chapter into fixed-time, bounded-time, and finite-time liveness. We present an algorithm for synthesis of minimally-interventive controllers that achieve liveness in rate-bounded hybrid systems.

Microprocessors and microcontrollers are now widely used in automobiles. Microprocessor systems contain sources of interrupt and interrupt service routines, which are software components executed in response to the assertion of an interrupt in hardware. A major problem in designing the software of microprocessor systems is the analytical treatment of interrupt latency. Because multiple interrupt service routines are executed on the same CPU, they compete for the CPU and interfere with each other's latency requirements. Here, interrupt latency is defined as the delay between the assertion of the interrupt in hardware and the start of execution of the associated interrupt service routine. It is estimated that 80% of intermittent bugs in small microprocessor software loads are due to improper treatment of interrupts. Until this work, there is no analytic method for analyzing a particular system to determine if it may violate interrupt latency requirements. There is also no reliable empirical method for ruling out the possibility of interrupt latency violations in a particular system, as they may occur under only very specific conditions. We use a newly developed hybrid system approach to solve this interrupt latency compatibility analysis problem. We have developed an efficient algorithm to determine if interrupt latency violations may occur in a particular system. A software tool that implements the algorithm is also being developed. With such software, we can easily check if interrupt latency constraints may be violated under any circumstances. If so, such software may also indicate how to modify the interrupts and interrupt service routines to avoid such violations. INTRODUCTION Microprocessor systems contain interrupt sources (ISs), which can request service from the processor (assert an interrupt), and must always have a software response (the execution of the corresponding software interrupt service routine, or ISR) starting within an interval of time (the maximum allowable interrupt latency, or AIL) after the assertion of the hardware interrupt. Because a processor may execute only one stream of instructions at a time, the execution of one ISR may delay the execution of another ISR until the first has completed. Hence, ISs and their associated ISRs interfere with each other’s interrupt latency requirements and may not be combined arbitrarily in the same microprocessor system without the possibility of the AIL being violated for some or all ISs. As a necessary condition to guarantee that a microprocessor system will always behave as intended, each IS must always be serviced by its corresponding ISR within the AIL. Verifying that the interrupt latency requirement is always satisfied for every IS is the interrupt latency compatibility problem that we address in this paper. The importance of the interrupt latency compatibility problem in microprocessor system design cannot be overstated. A system accidentally constructed so that interrupt latency incompatibilities exist has a high probability of exhibiting serious behavioral defects which are intermittent, because the conditions required to

In this paper, we study the control of Composite Hybrid Machines (CHMs) subject to safety specifications. CHMs are a fairly general class of hybrid systems modeled in modular fashion as the concurrent operation of Elementary Hybrid Machines (EHMs). The formalism has a well-defined synchronous-composition operation that permits the introduction of the controller as a component of the system. The task of a legal controller is to ensure that the system never exits a set of specified legal configurations. Among the legal controllers, we are particularly interested in designing a minimally-restrictive (or minimally-interventive) one, which interferes in the system's operation only when constraint violation is otherwise inevitable. Thus, when composed to operate concurrently with another legal controller, our controller will never interfere with the operation of the other. Therefore, a minimally-restrictive controller provides maximum flexibility in embedding additional controllers designed for other control objectives to operate concurrently, while eliminating the need to re-investigate or re-verify the legality of the composite controller. We describe in detail an algorithm for controller synthesis and examine through several examples questions associated with algorithm termination and controller existence.

In a series of seminal papers published between 1960 and 1965 [8–13] (see also [14, 15]), R.E. Kalman layed the foundations of what has since become known as Mathematical System Theory. The cornerstones of Kalman’s theory were the celebrated concepts of Controllability, Observability and (Canonical) realization. The first formal introduction of the concepts of controllability and observability as fundamental structural properties of (linear) systems was made by Kalman in [8, 9] and the canonical realization problem and its relation to controllability and observability was first studied extensively in [11]. The relation between the structure of canonical realizations and that of transfer matrices was investigated by Kalman extensively in [12]. The crucial insights in Kalman’s theory derived from the discovery that the concepts of controllability and observability are linked in an essential way to the system’s structure and that many of the system’s structural features are encoded in its controllable and observable behaviors.

We consider the problem of conflict resolution among multiple agents who navigate in a discrete shared resource environment. We present distributed algorithms that yield maximal solutions (Nash equilibria) for the conflict resolution problem in the two- and multiple- (more than two) agent cases.