Search

We present , a framework for the integration of modern verification tools in the context of AUTOSAR, a widely-used open standard for the development of automotive software systems. Our framework enables the automatic end-to-end verification of system-level properties using a compositional approach. It combines software model checking techniques for the verification of software components at the code level with a contract-based analysis for verifying their correct composition. In this paper, we present the tool through its application on a representative automotive case study, discussing the main functionalities provided and the results obtained.

The development of modern railways applications must be supported by trusted tools, able to cover the whole development process. In this paper we report on the research challenges underlying a comprehensive toolset for the design of computer-based interlocking systems. Following a VV development process, the framework adopts a clear separation between the abstract interlocking logic and the instantiations characterizing the single stations. The challenges include the definition of adequate specification languages, the generation of executable code and simulation infrastructure, traceability, test case generation, and formal verification.

Given a partially observable dynamic system and a diagnoser observing its evolution over time, diagnosability analysis formally verifies (at design time) if the diagnosis system will be able to infer (at runtime) the required information on the hidden part of the dynamic state. Diagnosability directly depends on the availability of observations, and can be guaranteed by different sets of sensors, possibly associated with different costs. In this paper, we tackle the problem of synthesizing observability requirements, i.e. automatically discovering a set of observations that is sufficient to guarantee diagnosability. We propose a novel approach with the following characterizing features. First, it fully covers a comprehensive formal framework for diagnosability analysis, and enables ranking configurations of observables in terms of cost, minimality, and diagnosability delay. Second, we propose two complementary algorithms for the synthesis of observables. Third, we describe an efficient implementation that takes full advantage of mature symbolic model checking techniques. The proposed approach is thoroughly evaluated over a comprehensive suite of benchmarks taken from the aerospace domain.

Deep space missions are characterized by severely constrained communication links. To meet the needs of future missions and increase their scientific return, future space systems will require an increased level of autonomy on-board. In this work, we propose a comprehensive approach to on-board autonomy. We rely on model-based reasoning, and we consider many important (on-line and off-line) reasoning capabilities such as plan generation, validation, execution and monitoring, runtime diagnosis, and fault detection, identification, and recovery. The controlled platform is represented symbolically, and the reasoning capabilities are seen as symbolic manipulation of such formal model. We have developed a prototype of our framework, and we have integrated it within an on-board Autonomous Reasoning Engine. Finally, we have evaluated our approach on three case-studies inspired by real-world projects and characterized it in terms of reliability, availability, and performance.

The system design process needs to cope with the increasing complexity and size of systems,motivating the replacement of labor intensivemanual techniques with automated and semi-automated approaches.Recently, formal methods techniques, such as model-based verification and safety assessment, have been increasingly used to model systems under fault and to analyze them, generating artifacts such as fault trees and FMEA tables. In this paper, we show how to apply model-based techniques to a realistic case study from the avionics domain: a high integrity power distribution system, the Triple Modular Generator (TMG). The TMG is composed of a redundant and reconfigurable plant and a controller that must guarantee a high level of reliability. The case study is a significant challenge, from the modeling perspective, since it implements a complex reconfiguration policy, specified via a number of requirements in natural language, including a set of mutually dependent and potentially conflicting priority constraints. Moreover, from the verification standpoint, the controller must be able to handle an exponential number of possible faulty configurations. Our contribution is twofold. First, we formalize and validate the requirements and, using a constraint-based modeling style, we synthesize a correct by construction controller, avoiding the enumeration of all possible fault configurations, as is currently done by manual approaches. Second, we describe a comprehensive methodology and process, supported by the xSAP safety analysis platform that targets the modeling and safety assessment of faulty systems. Using xSAP, we are able to automatically extract minimal cut sets for the TMG. We demonstrate the scalability of our approach by analyzing a parametric version of the TMG case study that contains more than 700 variables and 90 faults.

Automated temporal planning is the technology of choice when controlling systems that can execute more actions in parallel and when temporal constraints, such as deadlines, are needed in the model. One limitation of several action-based planning systems is that actions are modeled as intervals having conditions and effects only at the extremes and as invariants, but no conditions nor effects can be specified at arbitrary points or sub-intervals.In this paper, we address this limitation by providing an effective heuristic-search technique for temporal planning, allowing the definition of actions with conditions and effects at any arbitrary time within the action duration. We experimentally demonstrate that our approach is far better than standard encodings in PDDL 2.1 and is competitive with other approaches that can (directly or indirectly) represent intermediate action conditions or effects.

The field of Temporal Planning (TP) is receiving increasing interest for its many real-world applications. Most of the literature focuses on the TP problem of finding a plan, with algorithms that are not guaranteed to terminate when the problem admits no solution. In this paper, we present sound and complete decision procedures that address the dual problem of proving that no plan exists, which has important applications in oversubscription, model validation and optimization. We focus on the expressive and practically relevant semantics of action non-self-overlapping, recently proved to be PSPACE-complete. For this subclass, we propose two approaches: a reduction of the planning problem to model-checking of Timed Transition Systems, and a heuristic-search algorithm where temporal constraints are represented by Difference Bound Matrices. We implemented the approaches, and carried out an experimental evaluation against other state-of-the-art TP tools. On benchmarks that admit no plans, both approaches dramatically outperform the other planners, while the heuristic-search algorithm remains competitive on solvable benchmarks.

Diagnosability is a fundamental problem of partial observable systems in safety-critical design. Diagnosability verification checks if the observable part of system is sufficient to detect some faults. A counterexample to diagnosability may consist of infinitely many indistinguishable traces that differ in the occurrence of the fault. When the system under analysis is modeled as a Büchi automaton or finite-state Fair Transition System, this problem reduces to look for ribbon-shaped paths, i.e., fair paths with a loop in the middle.In this paper, we propose to solve the problem by extending the liveness-to-safety approach to look for lasso-shaped paths. The algorithm can be applied to various diagnosability conditions in a uniform way by changing the conditions on the loops. We implemented and evaluated the approach on various diagnosability benchmarks.

We present Norma, a tool for the modeling and analysis of Relay-based Railways Interlocking Systems (RRIS). Norma is the result of a research project funded by the Italian Railway Network, to support the reverse engineering and migration to computer-based technology of legacy RRIS. The frontend fully supports the graphical modeling of Italian RRIS, with a palette of over two hundred basic components, stubs to abstract RRIS subcircuits, and requirements in terms of formal properties. The internal component based representation is translated into highly optimized Timed nuXmv models, and supports various syntactic and semantic checks based on formal verification, simulation and test case generation. Norma is experimentally evaluated, demonstrating the practical support for the modelers, and the effectiveness of the underlying optimizations.

The analysis of legacy systems requires the automated extraction of high-level specifications. We propose a framework, called Abstraction Modulo Stability, for the analysis of transition systems operating in stable states, and responding with run-to-completion transactions to external stimuli. The abstraction captures the effects of external stimuli on the system state, and describes it in the form of a finite state machine. This approach is parametric on a set of predicates of interest and the definition of stability. We consider some possible stability definitions which yield different practically relevant abstractions, and propose a parametric algorithm for abstraction computation. The obtained FSM is extended with guards and effects on a given set of variables of interest. The framework is evaluated in terms of expressivity and adequacy within an industrial project with the Italian Railway Network, on reverse engineering tasks of relay-based interlocking circuits to extract specifications for a computer-based reimplementation.

Linear Temporal Logic ($$\mathsf {LTL}$$ LTL ) is one of the most popular temporal logics, that comes into play in a variety of branches of computer science. Its widespread use is also due to its strong foundational properties. One of them is Kamp’s theorem, showing that $$\mathsf {LTL}$$ LTL and the first-order theory of one successor ($$\mathsf {S1S}[\mathsf {FO}]$$ S 1 S [ FO ] ) are expressively equivalent. Safety and co-safety languages, where a finite prefix suffices to establish whether a word does not or does belong to the language, respectively, play a crucial role in lowering the complexity of problems like model checking and reactive synthesis for $$\mathsf {LTL}$$ LTL . $$\mathsf {Safety\text {-} \mathsf {LTL}}$$ Safety - LTL (resp., $$\mathsf {coSafety\text {-} \mathsf {LTL}}$$ coSafety - LTL ) is a fragment of $$\mathsf {LTL}$$ LTL where only universal (resp., existential) temporal modalities are allowed, that recognises safety (resp., co-safety) languages only. In this paper, we introduce a fragment of $$\mathsf {S1S}[\mathsf {FO}]$$ S 1 S [ FO ] , called $$\mathsf {Safety\text {-} FO}$$ Safety - FO , and its dual $$\mathsf {coSafety\text {-} FO}$$ coSafety - FO , which are expressively complete with regards to the $$\mathsf {LTL}$$ LTL -definable safety languages. In particular, we prove that they respectively characterise exactly $$\mathsf {Safety\text {-} \mathsf {LTL}}$$ Safety - LTL and $$\mathsf {coSafety\text {-} \mathsf {LTL}}$$ coSafety - LTL , a result that joins Kamp’s theorem, and provides a clearer view of the charactisations of (fragments of) $$\mathsf {LTL}$$ LTL in terms of first-order languages. In addition, it gives a direct, compact, and self-contained proof that any safety language definable in $$\mathsf {LTL}$$ LTL is definable in $$\mathsf {Safety\text {-} \mathsf {LTL}}$$ Safety - LTL as well. As a by-product, we obtain some interesting results on the expressive power of the weak tomorrow operator of $$\mathsf {Safety\text {-} \mathsf {LTL}}$$ Safety - LTL interpreted over finite and infinite traces.

To achieve practical execution, planners must produce temporal plans with some degree of run-time adaptability. Such plans can be expressed as Simple Temporal Networks (STN), that constrain the timing of action activations, and implicitly represent the space of choices for the plan executor.A first problem is to verify that all the executor choices allowed by the STN plan will be successful, i.e. the plan is valid. An even more important problem is to assess the effect of discrepancies between the model used for planning and the execution environment.We propose an approach to compute the “robustness envelope” (i.e., alternative action durations or resource consumption rates) of a given STN plan, for which the plan remains valid. Plans can have boolean and numeric variables as well as discrete and continuous change. We leverage Satisfiability Modulo Theories (SMT) to make the approach formal and practical.

Reliability is a fundamental property for critical systems. A thorough evaluation of the reliability is required by the certification procedures in various application domains, and it is important to support the exploration of the space of the design solutions. In this paper we propose a new, fully automated approach to the reliability analysis of complex redundant architectures. Given an abstract description of the architecture, the approach automatically extracts a fault tree and a symbolic reliability function, i.e. a program mapping the probability of fault of the basic components to the probability that the overall architecture deviates from the expected behavior. The proposed approach heavily relies on formal methods, by representing the architecture blocks as Uninterpreted Functions, and using the so-called miter construction to model the deviation from the nominal behavior. The extraction of all the deviation conditions is reduced to an AllSMT problem, and we extract the reliability function by traversing the Binary Decision Diagram corresponding to the quantified formula. Predicate abstraction is used to partition and speed up the computation. The approach has been implemented leveraging formal tools for model checking and safety assessment. A thorough experimental evaluation demonstrates its generality and effectiveness of the proposed techniques.

Power distribution grids are typically installed outdoors and are exposed to environmental conditions. When contamination accumulates in the structures of the network, there may be shutdowns caused by electrical arcs. To improve the reliability of the network, visual inspections of the electrical power system can be carried out; these inspections can be automated using computer vision techniques based on deep neural networks. Based on this need, this paper proposes the Semi-ProtoPNet deep learning model to classify defective structures in the power distribution networks. The Semi-ProtoPNet deep neural network does not perform convex optimization of its last dense layer to maintain the impact of the negative reasoning process on image classification. The negative reasoning process rejects the incorrect classes of an input image; for this reason, it is possible to carry out an analysis with a low number of images that have different backgrounds, which is one of the challenges of this type of analysis. Semi-ProtoPNet achieves an accuracy of 97.22%, being superior to VGG-13, VGG-16, VGG-19, ResNet-34, ResNet-50, ResNet-152, DenseNet-121, DenseNet-161, DenseNet-201, and also models of the same class such as ProtoPNet, NP-ProtoPNet, Gen-ProtoPNet, and Ps-ProtoPNet.

Proving existential properties of infinite-state systems (e.g. software non-termination, model checking of hybrid automata) comes with a key challenge: differently from the finite-state case, witnesses may not be in form of lasso-shaped fair paths. In this paper we propose an approach to automatically prove existential properties for infinite state transition systems, presenting witnesses in an indirect way. The approach is based on the notion of well-founded funnel, where a ranking function guarantees that the states in the source set are guaranteed to inevitably reach the destination set. We show that, under suitable conditions, a sequence of funnels ensures the existence of a fair path. We propose an algorithm that, working in an abstract space induced by a set of predicates, identifies candidate funnels, proves their well-foundedness, and searches for a sequencing order.

The process of developing civil aircraft and their related systems includes multiple phases of Preliminary Safety Assessment (PSA). An objective of PSA is to link the classification of failure conditions and effects (produced in the functional hazard analysis phases) to appropriate safety requirements for elements in the aircraft architecture. A complete and correct preliminary safety assessment phase avoids potentially costly revisions to the design late in the design process. Hence, automated ways to support PSA are an important challenge in modern aircraft design. A modern approach to conducting PSAs is via the use of abstract propagation models, that are basically hyper-graphs where arcs model the dependency among components, e.g. how the degradation of one component may lead to the degraded or failed operation of another. Such models are used for computingfailure propagations: the fault of a component may have multiple ramifications within the system, causing the malfunction of several interconnected components. A central aspect of this problem is that of identifying the minimal fault combinations, also referred to asminimal cut sets, that cause overall failures.In this paper we propose an expressive framework to model failure propagation, catering for multiple levels of degradation as well as cyclic and nondeterministic dependencies. We define a formal sequential semantics, and present an efficient SMT-based method for the analysis of failure propagation, able to enumerate cut sets that are minimal with respect to the order between levels of degradation. In contrast with the state of the art, the proposed approach is provably more expressive, and dramatically outperforms other systems when a comparison is possible.

In finite-state systems, true existential properties admit witnesses in form of lasso-shaped fair paths. When dealing with the infinite-state case (e.g. software non-termination, model checking of hybrid automata) this is no longer the case. In this paper, we propose a compositional approach for proving the existence of fair paths of infinite-state systems. First, we describe a formal approach to prove the existence of a non-empty under-approximation of the original system that only contains fair paths. Second, we define an automated procedure that, given a set of hints (in form of basic components), searches for a suitable composition proving the existence of a fair path. We experimentally evaluate the approach on examples taken from both software and hybrid systems, showing its wide applicability and expressiveness.

Runtime Verification (RV) basically means monitoring an execution trace of a system under scrutiny and checking if the trace satisfies or violates a specification. In Assumption-Based Runtime Verification (ABRV), runtime monitors may be synthesized from not only the specification but also a system model (either full or partial), which represents the assumptions on which the input traces are expected to follow. With assumptions the monitor can additionally check if the input traces actually follow the assumptions. Some previous research has shown that monitors under assumptions can be more precise or even predictive, while non-monitorable specifications may become monitorable under assumptions.

Incremental linearization is a conceptually simple, yet effective, technique that we have recently proposed for solving SMT problems on the theories of non-linear arithmetic over the reals and the integers. Optimization Modulo Theories (OMT) is an important extension of SMT which allows for finding models that optimize given objective functions. In this paper, we show how incremental linearization can be extended to OMT in a simple way, producing an incomplete though effective OMT procedure. We describe the main ideas and algorithms, we provide an implementation within the OptiMathSAT OMT solver, and perform an empirical evaluation. The results support the effectiveness of the approach.

Stability is a fundamental requirement of dynamical systems. Most of the works concentrate on verifying stability for a given stability region. In this paper we tackle the problem of synthesizing \(\mathbb {P}\) -stable abstractions. Intuitively, the \(\mathbb {P}\)-stable abstraction of an open dynamical system characterizes the transitions between stability regions in response to external inputs. The stability regions are not given - rather, they are synthesized as the tightest representation with respect to a given set of relevant predicates \(\mathbb {P}\). A \(\mathbb {P}\)-stable abstraction is enriched by timing information derived from the duration of stabilization.

This paper describes a model-based flow for the development of Interlocking Systems. The flow starts from a set of specifications in Controlled Natural Language (CNL), that are close to the jargon adopted in by domain experts, but fully formal. From the CNL, a complete SysML specification is extracted, leveraging various forms of diagrams, and enabling automated code generation. Several formal verification methods are supported. A complementary part of the flow supports the extraction of formal properties from legacy Interlocking Systems designed as Relay circuits. The flow is implemented in a comprehensive toolset, and is currently used by railway experts.

nuXmv is a well-known symbolic model checker, which implements various state-of-the-art algorithms for the analysis of finite- and infinite-state transition systems and temporal logics. In this paper, we present a new version that supports timed systems and logics over continuous super-dense semantics. The system specification was extended with clocks to constrain the timed evolution. The support for temporal properties has been expanded to include \(\textsc {MTL}_{0,\infty }\) formulas with parametric intervals. The analysis is performed via a reduction to verification problems in the discrete-time case. The internal representation of traces has been extended to go beyond the lasso-shaped form, to take into account the possible divergence of clocks. We evaluated the new features by comparing nuXmv with other verification tools for timed automata and \(\textsc {MTL}_{0,\infty }\), considering different benchmarks from the literature. The results show that nuXmv is competitive with and in many cases performs better than state-of-the-art tools, especially on validity problems for \(\textsc {MTL}_{0,\infty }\).

We consider Runtime Verification (RV) based on Propositional Linear Temporal Logic (LTL) with both future and past temporal operators. We generalize the framework to monitor partially observable systems using models of the system under scrutiny (SUS) as assumptions for reasoning on the non-observable or future behaviors of the SUS. The observations are general predicates over the SUS, thus both static and dynamic sets of observables are supported. Furthermore, the monitors are resettable, i.e. able to evaluate any LTL property at arbitrary positions of the input trace (roughly speaking, \([\![u,i\models \varphi ]\!]\) can be evaluated for any u and i with the underlying assumptions taken into account). We present a symbolic monitoring algorithm that can be efficiently implemented using BDD. It is proven correct and the monitor can be double-checked by model checking. As a by-product, we give the first automata-based monitoring algorithm for Past-Time LTL. Beside feasibility and effectiveness of our approach, we also demonstrate that, under certain assumptions the monitors of some properties are predictive.

In order to be resilient, a system must be adaptable. Trustworthy adaptation requires that a system can be dynamically reconfigured at run-time without compromising the robustness and integrity of the system. Adaptive MILS extends MILS, a successful paradigm for rigorously developed and assured composable static systems, with reconfiguration mechanisms and a framework within which those mechanisms may be safely and securely employed for adaptation.

Hybrid traces are useful to describe behaviors of dynamic systems where continuous and discrete evolutions are combined. The ability to represent sets of traces by means of formulas in temporal logic has recently found important applications in various fields, such as requirements analysis, compositional verification, and contract-based design. In this paper we present HRELTL, a temporal logic to characterize hybrid traces. The logic is highly expressive: it allows the description of continuous behaviors, by expressing mathematical constraints over derivatives, and discrete behaviors, by constraining values of variables across instantaneous transitions. HRELTL combines the power of temporal operators and regular expressions, and enjoys important properties such as sampling invariance. We demonstrate that the satisfiability problem for a fragment of HRELTL allows for a satisfiability-preserving reduction to RELTL(RA), a logic over discrete traces with atoms in non-linear Real Arithmetic for which automated reasoning procedures are being developed.

In this paper, we propose to extend First-Order Linear-time Temporal Logic with Past adding two operators “at next” and “at last”, which take in input a term and a formula and return the value of the term at the next state in the future or last state in the past in which the formula holds. The new logic, named LTL-EF, can be interpreted with different models of time (including discrete, dense, and super-dense time) and with different first-order theories (a la Satisfiability Modulo Theories (SMT)). We show that the “at next” and “at last” can encode (first-order) MTL 0 , ∞ with counting. We provide rewriting procedures to reduce the satisfiability problem to the discrete-time case (to leverage on the mature state-of-the-art corresponding verification techniques) and to remove the extra functional symbols. We implemented these techniques in the nuXmv model checker enabling the analysis of LTL-EF and MTL 0 , ∞ based on SMT-based model checking. We show the feasibility of the approach experimenting with several non-trivial valid and satisfiable formulas.

Symbolic execution systematically explores program paths by solving path conditions --- formulas over symbolic variables. Typically, the symbolic variables range over numbers, arrays and strings. We introduce symbolic execution with existential second-order constraints --- an extension of traditional symbolic execution that allows symbolic variables to range over functions whose interpretations are restricted by a user-defined language. The aims of this new technique are twofold. First, it offers a general analysis framework that can be applied in multiple domains such as program repair and library modelling. Secondly, it addresses the path explosion problem of traditional first-order symbolic execution in certain applications. To realize this technique, we integrate symbolic execution with program synthesis. Specifically, we propose a method of second-order constraint solving that provides efficient proofs of unsatisfiability, which is critical for the performance of symbolic execution. Our evaluation shows that the proposed technique (1) helps to repair programs with loops by mitigating the path explosion, (2) can enable analysis of applications written against unavailable libraries by modelling these libraries from the usage context.

Relay Interlocking Systems (RIS) are analog electromechanical networks traditionally applied in the safety-critical domain of railway signaling. RIS consist of networks of interconnected components such as power supplies, contacts, resistances, and electrically-controlled contacts (i.e. the relays). Due to cost and flexibility needs, RIS are progressively being replaced by equivalent computer-based systems. Unfortunately, RIS are often legacy systems, hard to understand at an abstract level, hence the valuable information they encoded in them is not available.In this paper, we propose a methodology and a tool chain to analyze and understand legacy RIS. A RIS is reduced to a Switched Multi-Domain Kirchhoff Network (SMDKN), which is in turn compiled into hybrid automata. SMT-based model checking supports various forms of formal analyses for SMDKN. The approach is based on the modeling of the RIS analog signals (i.e. currents and voltages) over continuous time, and their mapping in terms of railways control actions. Starting from the diagram representation, we overcome a key limitation of previous approaches based on purely Boolean models, i.e. the presence of spurious behaviors. The evaluation of the tool chain on a set of industrial-size railway RIS demonstrates practical scalability.

Satisfiability Modulo Theories (SMT) is the problem of deciding the satisfiability of a first-order formula with respect to some theory or combination of theories. In this paper, we overview our recent approach called Incremental Linearization, which successfully tackles the problems of SMT over the theories of nonlinear arithmetic over the reals (NRA), nonlinear arithmetic over the integers (NIA) and their combination, and of NRA augmented with transcendental (exponential and trigonometric) functions (NTA). Moreover, we showcase some of the experimental results and outline interesting future directions.

Symbolic Computation and Satisfiability Checking are two research areas, both having their individual scientific focus but with common interests, e.g., in the development, implementation and application of decision procedures for arithmetic theories. Despite their commonalities, the two communities are rather weakly connected. The aim of the SC-square initiative is to strengthen the connection between these communities by creating common platforms, initiating interaction and exchange, identifying common challenges, and developing a common roadmap from theory along the way to tools and (industrial) applications.

This report presents results of a friendly competition for formal verification of continuous and hybrid systems with piecewise constant dynamics. The friendly competition took place as part of the workshop Applied Verification for Continuous and Hybrid Systems (ARCH) in 2017. In its first edition, four tools have been applied to solve five different benchmark problems in the category for piecewise constant dynamics: BACH, Lyse, PHAVer, and VeriSiMPL. The result is a snapshot of the current landscape of tools and the types of benchmarks they are particularly suited for. Due to the diversity of problems, we are not ranking tools, yet the presented results probably provide the most complete assessment of tools for the safety verification of continuous and hybrid systems with piecewise constant dynamics up to this date.

Incremental linearization is a conceptually simple, yet effective, technique that we have recently proposed for solving SMT problems over nonlinear real arithmetic constraints. In this paper, we show how the same approach can be applied successfully also to the harder case of nonlinear integer arithmetic problems. We describe in detail our implementation of the basic ideas inside the MathSAT SMT solver, and evaluate its effectiveness with an extensive experimental analysis over all nonlinear integer benchmarks in SMT-LIB. Our results show that MathSAT is very competitive with (and often outperforms) state-of-the-art SMT solvers based on alternative techniques.

We propose a novel approach to the formal specification and verification of dynamic architectures that are at the core of adaptive systems such as critical infrastructure protection. Key features include run-time reconfiguration based on adding and removing components and connections, resulting in systems with unbounded number of components. We provide a logic-based specification of a Dynamic Parametrized Architecture (DPA), where parameters represent the infinite-state space of possible configurations, and first-order formulas represent the sets of initial configurations and reconfiguration transitions. We encode information flow properties as reachability problems of such DPAs, define a translation into an array-based transition system, and use a Satisfiability Modulo Theories (SMT)-based model checker to tackle a number of case studies.

The framework of temporal problems with uncertainty (TPU) is useful to express temporal constraints over a set of activities subject to uncertain (and uncontrollable) duration. In this work, we focus on the most general class of TPU, namely disjunctive TPU (DTPU), and consider the case of weak controllability, that allows one to model problems arising in practical scenarios (e.g. on-line scheduling). We first tackle the decision problem, i.e. whether there exists a schedule of the activities that, depending on the uncertainty, satisfies all the constraints. We propose a logical approach, based on the reduction to a problem of Satisfiability Modulo Theories (SMT), in the theory of Linear Real Arithmetic with Quantifiers. This results in the first implemented solver for weak controllability of DTPUs. Then, we tackle the problem of synthesizing control strategies for scheduling the activities. We focus on strategies that are amenable for efficient execution. We prove that linear strategies are not always sufficient, even in the sub-case of simple TPU (STPU), while piecewise-linear strategies, that are multiple conditionally-applied linear strategies, are always sufficient. We present several algorithms for the synthesis of linear and piecewise-linear strategies, in case of STPU and of DTPU. All the algorithms are implemented on top of SMT solvers. We provide experimental evidence of the scalability of the proposed techniques, with dramatic speed-ups in strategy execution compared to on-line reasoning.