All times indicated below are in Central Time (CT).
Beijing is 13 hours ahead of CT.
Milano is 7 hours ahead of CT
Closed-loop verification of cyber-physical systems with neural network controllers offers strong safety guarantees under certain assumptions. It is, however, difficult to determine whether these guarantees apply at run time because verification assumptions may be violated. To predict safety violations in a verified system, we propose a three-step framework for monitoring the confidence in verification assumptions. First, we represent the sufficient condition for verified safety with a propositional logical formula over assumptions. Second, we build calibrated confidence monitors that evaluate the probability that each assumption holds. Third, we obtain the confidence in the verification guarantees by composing the assumption monitors using a composition function suitable for the logical formula. Our framework provides theoretical bounds on the calibration and conservatism of compositional monitors. In two case studies, we demonstrate that the composed monitors improve over their constituents and successfully predict safety violations.
This paper presents a new framework for generating test-case scenarios for autonomous vehicles. We address two challenges in automatic test-case generation: first, a formal notion of test-case complexity, and second, an algorithm to generate more-complex test-cases. We characterize the complexity of a test-case by its set of solutions, and compare two complexities by the subset relation. The novelty of our definition is that it only relies on the pass-fail criteria of the test-case, rather than indirect or subjective assessments of what may challenge an ego vehicle to pass a test-case. Given a test-case, we model the problem of generating a more complex test-case as a constraint-satisfaction search problem. The search variables are the changes to the given test-case, and the search constraints define a solution to the search problem. The constraints include steering geometry of cars, the geometry of lanes, the shape of cars, traffic rules, bounds on longitudinal acceleration of cars, etc. To conquer the computational challenge, we divide the constraints to three categories and satisfy them with simulation, answer set programming, and SMT solving. We have implemented our algorithm using the Scenic libraries and the CARLA simulator and generate test-cases for several 3-way and 4-way intersections with different topologies. Our experiments demonstrate that both CARLA’s autopilot and autopilot-plus-RSS Responsibility-Sensitive Safety) can fail as the complexity of test-cases increase.
Fuzz testing is an indispensable test-generation tool in software security. Fuzz testing uses automated directed randomness to explore a variety of execution paths in software, trying to expose defects such as buffer overflows. Since cyber-physical systems (CPS) are often safety-critical, testing models of CPS can also expose faults. However, while existing coverage-guided fuzz testing methods are effective for software, results can be disappointing when applied to CPS, where systems have continuous states and inputs are applied at different points in time. In this work, we propose three changes to customize coverage-guided fuzz testing methods to better leverage characteristics of CPS. First, we introduce a notion of coverage that be used to evaluate a fuzz testing algorithm’s effectiveness for a particular CPS, analogous to often-used code coverage metrics of a software system. Second, this modified coverage metric is used in a customized power schedule, which selects which previous input sequences hold the most promise to find failures in new system states. Third, we modify the input mutation strategy used to reason with the causal nature of a CPS. We call the approach CPSFuzz and evaluate it on a simulation environment used for the F1TENTH autonomous car racing competition, attempting to find collisions during head-to-head racing. Compared with both using existing software fuzz testing tools and random test generation, CPSFuzz generates more crashes at different positions around the track.
Simulation-based testing of autonomous vehicles (AVs) has become an essential complement to road testing to ensure safety. Consequently, substantial research has focused on searching for failure scenarios in simulation. However, a fundamental question remains: are AV failure scenarios identified in simulation meaningful in reality — i.e., are they reproducible on the real system? Due to the sim-to-real gap arising from discrepancies between simulated and real sensor data, a failure scenario identified in simulation can be either a spurious artifact of the synthetic sensor data or an actual failure that persists with real sensor data. One approach to validate simulated failure scenarios is to identify instances of the scenario in a corpus of real data, and check if the failure persists on the real data. Towards this end, we propose a formal definition of what it means for a labelled data point to match an abstract scenario, encoded as a scenario program using the SCENIC probabilistic programming language. Using this definition, we develop a querying algorithm which, given a scenario program and a labelled dataset, finds the subset of the data matching the scenario. Experiments demonstrate that our algorithm is accurate and efficient on a variety of realistic traffic scenarios, and scales to a reasonable number of agents.
Tactile Internet (TI) enables the transfer of human skills across the Internet by enabling teleoperation with force feedback. Advancements are being made rapidly at several fronts to realize a functional TI soon. Generally, TI expects faithful reproduction of the operator’s action at the other end, where a robotic arm emulates it while providing force feedback to the operator. Performance of TI is usually characterized using objective metrics such as network delay, RMSE, and packet losses. Pari passu, subjective evaluations are used as additional validation, and performance evaluation itself is not primarily based on user experience. Hence objective evaluation, which generally minimizes error (signal mismatch) is oblivious to subjective experience. In this paper, we argue that user-centric designs of TI solutions are necessary. We first consider a few common TI errors and examine their perceivability. The idea is to reduce the impact of perceivable errors and exploit the imperceivable errors for our advantage, while the objective metrics may indicate that the errors are high. To harness the imperceivable errors, we design Adaptive Offset Framework (AOF) to improve the TI signal reconstruction under realistic network settings. We use AOF to highlight the contradictory inferences drawn by objective and subjective evaluations while realizing that subjective evaluations are closer to ground truth. This strongly suggests the existence of blind spots of objective measures’. Further, we show that AOF significantly improves the user grade, up to 3 points (on a scale of 10) in comparison with the standard reconstruction method.
The Sounds of New York City (SONYC) wireless sensor network(WSN) has been fielded in Manhattan and Brooklyn over the past five years, as part of a larger human-in-the-loop cyberphysical control system for monitoring, analyzing, and mitigating urban noise pollution. We describe the evolution of the 2-tier SONYC WSN from an acoustic data collection fabric into a 3-tier in situ noise complaint monitoring WSN, and its current evaluation. The added tier consists of long range (LoRA), multi-hop networks of a new low-power acoustic mote, MKII (“Mach 2”), that we have designed and fabricated. MKII motes are notable in three ways: First, they advance machine learning capability at mote-scale in this application domain by introducing a real-time CNN embedding model that is competitive with alternatives while also requiring 10×lesser training data and∼2 orders of magnitude fewer run-time resources. Second, they are conveniently deployed relatively far from higher tier base station nodes without assuming power or network infrastructure support at operationally relevant sites(such as construction zones), yielding a relatively low cost solution.And third, their networking is frequency agile, unlike conventionalLoRa networks: it tolerates in a distributed, self-stabilizing way the variable external interference and link fading in the cluttered 902-928MHz ISM band urban environment by dynamically choosing good frequencies using an efficient new method that combines passive and active measurements.
Although autonomous vehicles (AVs) are expected to revolutionize transportation, robust perception across a wide range of driving contexts remains a significant challenge. Techniques to fuse sensor data from camera, radar, and lidar sensors have been proposed to improve AV perception. However, existing methods are insufficiently robust in difficult driving contexts (e.g., bad weather, low light, sensor obstruction) due to rigidity in their fusion implementations. These methods fall into two broad categories: (i) early fusion, which fails when sensor data is noisy or obscured, and (ii) late fusion, which cannot leverage features from multiple sensors and thus produces worse estimates. To address these limitations, we propose HydraFusion a selective sensor fusion framework that learns to identify the current driving context and fuses the best combination of sensors to maximize robustness without compromising efficiency. HydraFusion is the first approach to propose dynamically adjusting between early fusion, late fusion, and combinations in-between, thus varying both how and when fusion is applied. We show that, on average, HydraFusion outperforms early and late fusion approaches by 13.66% and 14.54%, respectively, without increasing computational complexity or energy consumption on the industry-standard Nvidia Drive PX2 AV hardware platform. We also propose and evaluate both static and deep-learning-based context identification strategies. Our open-source code and model implementation are available at https://anonymous.4open.science/r/hydrafusion/.
Deep brain stimulation (DBS) is an effective procedure to treat motor symptoms caused by nervous system disorders such as Parkinson’s disease (PD). Although existing implantable DBS devices can suppress PD symptoms by delivering fixed periodic stimuli to the Basal Ganglia (BG) region of the brain, they are considered inefficient in terms of energy and could cause side-effects. Recently, reinforcement learning (RL)-based DBS controllers have been developed to achieve both stimulation efficacy and energy efficiency, by adapting stimulation parameters (e.g., pattern and frequency of stimulation pulses) to the changes in neuronal activity. However, RL methods usually provide limited safety and performance guarantees, and directly deploying them on patients may be hindered due to clinical regulations. Thus, in this work, we introduce a model-based offline policy evaluation (OPE) methodology to estimate the performance of RL policies using historical data. As a first step, the BG region of the brain is modeled as a Markov decision process (MDP). Then, a deep latent MDP (DL-MDP) model is learned using variational inference and previously collected control trajectories. The performance of RL controllers is then evaluated on the DL-MDP models instead of patients directly, ensuring safety of the evaluation process. Further, we show that our method can be integrated into offline RL frameworks, improving control performance when limited training data are provided. We illustrate the use of our methodology on a computational Basal Ganglia model (BGM); we show that it accurately estimates the expected returns of controllers trained following state-of-the-art RL frameworks, outperforming existing OPE methods designed for general applications.
Autonomous systems with machine learning-based perception can exhibit unpredictable behaviors that are difficult to quantify, let alone verify. Such behaviors are convenient to capture in probabilistic models, but model checking of such models is difficult to scale — largely due to the non-determinism added to models as a prerequisite for provable conservatism. Statistical model checking (SMC) has been proposed to address the scalability issue. However it requires large amounts of data to account for the aforementioned non-determinism, which in turn limits its scalability. This work introduces a general technique for reduction of non-determinism based on assumptions of “monotonic safety”, which define a partial order between system states in terms of their probabilities of being safe. We exploit these assumptions to remove non-determinism from controller\/plant models to drastically speed up probabilistic model checking and statistical model checking while providing provably conservative estimates as long as the safety is indeed monotonic. Our experiments demonstrate model-checking speed-ups of an order of magnitude while maintaining acceptable accuracy and require much less data for accurate estimates when running SMC — even when monotonic safety does not perfectly hold and provable conservatism is not achieved.
Resilient cyber-physical systems (CPS) must ensure safety and perform required tasks in the presence of malicious cyber attacks. Recently, restart-based defenses have been proposed in which a CPS mitigates attacks by reverting to an initial safe state. In this paper, we consider a class of reactive restart approaches for CPS under malicious attacks with verifiable safety guarantees. We consider a setting where the controllers are engineered to crash and reboot following faults or attacks. We present a hybrid system model that captures the trade-off between security, availability, and safety of the CPS due to the reactive restart. We develop sufficient conditions under which an affine controller provides verifiable safety guarantees for the physical plant using a barrier certificate approach. We synthesize safety-critical controllers using control barrier functions to guarantee system safety under given timing parameters. We present two case studies on the proposed approach using a warehouse temperature control system and a two-dimensional non-linear system. Our proposed approach guarantees the safety for both cases.
In this paper, we proposa a new approach for statistical verification of parametric black-box CPS models with a user-provided distribution on the model parameters. Our technique uses model simulations to learn surrogate models, and uses conformal in-ference to provide probabilistic guarantees on the satisfaction of a given STL property. Additionally, we can provide prediction intervals containing the quantitative satisfaction values of the given STL property for any user-specified confidence level. We also propose a refinement procedure based on Gaussian Process (GP)-based surrogate models for obtaining fine-grained probabilistic guarantees over sub-regions in the parameter space. This in turn enables the CPS designer to choose assured validity domains in the parameter space for safety-critical applications. Finally,we demonstrate the efficacy of our technique on several CPS models.
We present a runtime assurance (RTA) mechanism for ensuring safety of a controlled dynamical system and an application to collision avoidance of two unmanned aerial vehicles (UAVs). We consider a dynamical system controlled by an unverified and potentially unsafe primary controller that might, e.g., lead to collision. The proposed RTA mechanism computes at each time the reachable set of the system under a backup control law. We then develop a novel optimization problem based on control barrier functions that filters the primary controller when necessary in order to keep the system’s reachable set within reach of a known, but conservative, safe region. The theory of mixed monotone systems is leveraged for efficient reachable set computation and to achieve a tractable optimization formulation. We demonstrate the proposed RTA mechanism on a dual multirotor UAV case study which requires a fast controller update rate as a result of the small time-scale rotational dynamics. In implementation, the algorithm computes the reachable set of an eight dimensional dynamical system in less than five milliseconds and solves the optimization problem in under one millisecond, yielding a controller update rate of 100Hz.
Neural networks have shown great promises in planning, control, and general decision making for learning-enabled cyber-physical systems (LE-CPSs), especially in improving performance under complex scenarios. However, it is very challenging to formally analyze the behavior of neural network based planners for ensuring system safety, which significantly impedes their applications in safety-critical domains such as autonomous driving. In this work, we propose a hierarchical neural network based planner that analyzes the underlying physical scenarios of the system and learns a system-level behavior planning scheme with multiple scenario-specific motion-planning strategies. We then develop an efficient verification method that incorporates overapproximation of the system state reachable set and novel partition and union techniques for formally ensuring system safety under our physics-aware planner. With theoretical analysis, we show that considering the different physical scenarios and building a hierarchical planner based on such analysis may improve system safety and verifiability. We also empirically demonstrate the effectiveness of our approach and its advantage over other baselines in practical case studies of unprotected left turn and highway merging, two common challenging safety-critical tasks in autonomous driving.
Many transit agencies operating paratransit and microtransit services have to respond to trip requests that arrive in real-time, which entails solving hard combinatorial and sequential decision-making problems under uncertainty. To avoid decisions that lead to significant inefficiency in the long term, vehicles should be allocated to requests by optimizing a non-myopic utility function or by batching requests together and optimizing a myopic utility function. While the former approach is typically offline, the latter can be performed online. We point out two major issues with such approaches when applied to paratransit services in practice. First, it is difficult to batch paratransit requests together as they are temporally sparse. Second, the environment in which transit agencies operate changes dynamically (e.g., traffic conditions can change over time), causing the estimates that are learned offline to become stale. To address these challenges, we propose a fully online approach to solve the dynamic vehicle routing problem (DVRP) with time windows and stochastic trip requests that is robust to changing environmental dynamics by construction. We focus on scenarios where requests are relatively sparse—our problem is motivated by applications to paratransit services. We formulate DVRP as a Markov decision process and use Monte Carlo tree search to compute near-optimal actions for any given state. Accounting for stochastic requests while optimizing a non-myopic utility function is computationally challenging; indeed, the action space for such a problem is intractably large in practice. To tackle the large action space, we leverage the structure of the problem to design heuristics that can sample promising actions for the tree search. Our experiments using real-world data from our partner agency show that the proposed approach outperforms existing state-of-the-art approaches both in terms of performance and robustness.
Deep reinforcement learning (DRL) has shown good performance in tackling Markov decision process (MDP) problems. As DRL optimizes a long-term reward, it is a promising approach to improving the energy efficiency of data center cooling. However, enforcement of thermal safety constraint during DRL’s state exploration is a main challenge. The widely adopted reward shaping approach adds negative reward when the exploratory action results in unsafety. Thus, it needs to experience sufficient unsafe states before it learns how to prevent unsafety. In this paper, we propose a safety-aware DRL framework for single-hall data center cooling control. It applies offline imitation learning and online post-hoc rectification to holistically prevent thermal unsafety during online DRL. In particular, the post-hoc rectification searches for the minimum modification to the DRL-recommended action such that the rectified action will not result in unsafety. The rectification is designed based on a thermal state transition model that is fitted using historical safe operation traces and able to extrapolate the transitions to unsafe states explored by DRL. Extensive evaluation for chilled water and direct expansion cooled data centers in two climate conditions shows that our approach saves 18\\% to 26\\% power compared with conventional control, reduces safety violations by 85\\% to 99\\% compared with reward shaping.
Complex real-world applications of cyber-physical systems give rise to the need for multi-objective controller synthesis, which concerns the problem of computing an optimal controller subject to multiple (possibly conflicting) criteria. The relative importance of objectives is often specified by human decision-makers. However, there is inherent uncertainty in human preferences (e.g., due to artifacts resulting from different preference elicitation methods). In this paper, we formalize the notion of uncertain human preferences, and present a novel approach that accounts for this uncertainty in the context of multi-objective controller synthesis for Markov decision processes (MDPs). Our approach is based on mixed-integer linear programming and synthesizes an optimally permissive multi-strategy that satisfies uncertain human preferences with respect to a multi-objective property. Experimental results on a range of large case studies show that the proposed approach is feasible and scalable across varying MDP model sizes and uncertainty levels of human preferences. Evaluation via an online user study also demonstrates the quality and benefits of the synthesized controllers.
Buildings account for 30% of energy use worldwide, and approxi-
mately half of it is ascribed to HVAC systems. Reinforcement Learn-
ing (RL) has improved upon traditional control methods in increas-
ing the energy efficiency of HVAC systems. However, prior works
use online RL methods that require configuring complex thermal
simulators to train or use historical data-driven thermal models that
can take at least 10^4 time steps to reach rule-based performance
Also, due to the distribution drift from simulator to real buildings,
RL solutions are therefore seldom deployed in the real world. On
the other hand, batch RL methods can learn from the historical
data and improve upon the existing policy without any interactions
with the real buildings or simulators during the training. With the
existing rule-based policy as the priors, the policies learned with
batch RL are better than the existing control from the first day of
deployment with very few training steps compared with online
Our algorithm incorporates a Kullback-Leibler (KL) regulariza-
tion term to penalize policies that deviate far from the previous
ones. We evaluate our framework on a real multi-zone, multi-floor
building—it achieves 7.2% in energy reduction cf. the state-of-the-
art batch RL method, and outperforms other BRL methods in occu-
pants’ thermal comfort, and 16.7% energy reduction compared to
the default rule-based control.
Full program for ICCPS Posters and Demo Session(s) listed [Here]
Full program for ICCPS Posters and Demo Session(s) listed [Here]
This paper explores and evaluates the potential of deep neural network (DNN)-based machine learning algorithms on embedded many-core processors in cyber-physical systems, such as self-driving systems. To run applications in embedded systems, a platform characterized by low power consumption with high accuracy and real-time performance is required. Furthermore, a platform is required that allows the coexistence of DNN applications and other applications, including conventional real-time control software, to enable advanced embedded systems, such as self-driving systems. Clustered many-core processors, such as Kalray MPPA3-80 Coolidge, can run multiple applications on a single platform because each cluster can run applications independently. Moreover, MPPA3-80 integrates multiple arithmetic elements that operate at low frequencies, thereby enabling high performance and low power consumption comparable to that of embedded graphics processing units. Furthermore, Kalray Neural Network (KaNN) code generator, a deep learning inference compiler for the MPPA3-80 platform, can efficiently perform DNN inference on MPPA3-80. This paper evaluates DNN models, including You Only Look Once (YOLO)-based and Single Shot MultiBox Detector (SSD)-based models, on MPPA3-80. The evaluation examines the frame rate and power consumption in relation to the size of the input image, the computational accuracy, and the number of clusters.
In this paper, we present a system called Versatile Autonomous Racquet Sports Machine (VaRSM in short). VaRSM can play table tennis, tennis and badminton balls with respective rackets. There are two major challenges in building VaRSM; first, VaRSM must be able to strike and return balls of variable speed and power on fields of varied size with various racquet motions; second, because of the balls’ high speed, VaRSM must track and predict their trajecto- ries as well as move its body in extremely short periods of time. To address these challenges, we design several innovative tech- nologies, which can be grouped into the physical hardware module and the control software module. In the physical hardware module, we create a high speed swerve-drive platform and a high-flexibility rac- quet arm, both with configurable “integrated drive units” (IDU). In the control software module, we take full advantage of the ma- chine’s physical abilities and develop a proactive progressive con- trol method to achieve early ball trajectory prediction, quick strik- ing decision making, and fast yet stable mobile platform and racquet arm motion. We build a prototype system based on these technologies. Our experiments demonstrate VaRSM is able to strike and return table tennis, tennis and badminton balls with high success rates and is capable of playing with human players. To our knowledge, VaRSM is the first machine able to play three different ball games. The machine may hold great significance in education, research, economy, and society. Youtube link
Modern smart cities are focusing on smart transportation solutions to detect and mitigate the effects of various traffic incidents in the city. To materialize this, road side units and ambient transportation sensors are being deployed to collect vehicular data that provides real-time traffic monitoring. In this paper, we first propose a real-time data-driven anomaly-based traffic incident detection framework for a city scale smart transportation system. Specifically, we propose an incremental region growing approximation algorithm for optimal spatio-temporal clustering of road segments and their data; such that road segments are strategically divided into highly correlated clusters. The highly correlated clusters enable identifying a Pythagorean Mean-based invariant as an anomaly detection metric that is highly stable under no incidents but show deviation in the presence of incidents. We learn the bounds of the invariants in a robust manner such that anomaly detection can generalize to unseen events, even when learning from real noisy data. We perform extensive experimental validation using mobility data collected from the City of Nashville, Tennessee, and prove that the method is able to detect incidents within each cluster in real-time.
The use of learning based components in cyber-physical systems (CPS) has created a gamut of possible avenues to use high dimensional real world signals generated from sensors like camera and LiDAR. The ability to process such signals can be largely attributed to the adoption of high-capacity function approximators like deep neural networks. However this does not come without its potential perils. The pitfalls arise from possible over-fitting, and subsequent unsafe behavior when exposed to unknown environments. One challenge is that, in high dimensional input spaces it is almost impossible to experience enough training data in the design phase. What is required here, is an efficient way to flag out-of-distribution (OOD) samples that is precise enough to not raise too many false alarms. In addition, the system needs to be able to detect these in a computationally efficient manner at runtime. In this paper, our proposal is to build good representations for in-distribution data. We introduce the idea of a memory bank to store prototypical samples from the input space. We use these memories to compute probability density estimates using kernel density estimation techniques. We evaluate our technique on two challenging scenarios : a self-driving car setting implemented inside the simulator CARLA with image inputs, and an autonomous racing car navigation setting, with LiDAR inputs. In both settings it was observed that a deviation from in-distribution setting can potentially lead to deviation from safe behavior. An added benefit of using training samples as memories to detect out-of-distribution input is that the system is interpretable to a human operator. Explanations of this nature is generally hard to obtain from pure deep learning based alternatives.
Obfuscation can be used by dynamic systems to ensure private and secure communication over networks vulnerable to eavesdroppers. Balancing the utility of sending information to intended recipients and privacy by hiding information from unintended recipients presents an interesting challenge. We propose a new framework for obfuscation that includes an inference interface to allow intended recipients to interpret obfuscated information. We model the security of the obfuscation with opacity, a formal notion of plausible deniability. Using techniques from distributed reactive synthesis, we show how to automatically design a privacy-enforcing obfuscator along with the inference interface that is given to intended recipients to use as a “key”. We demonstrate this approach by enforcing privacy while maintaining utility in a contact tracing model.
The increasing proliferation of cyber-physical systems in a multitude of applications presents a pressing need for effective methods of securing such devices. Many such systems are subject to tight timing constraints, which are poorly suited to traditional security methods due to the large runtime overhead and execution time variation introduced. However, the regular (and well documented) timing specifications of real-time systems open up new avenues with which such systems can be secured. This paper contributes T-SYS, a timed-system method of detecting intrusions into real-time systems via timing anomalies. A prototype implementation of T-SYS is integrated into a commercial real-time operating system (RTOS) in order to demonstrate its feasibility. Further, a compiler-based tool is developed to realize a T-SYS implementation with elastic timing bounds. This tool supports integration of T-SYS protection into applications as well as the RTOS the kernel itself. Results on an ARM hardware platform with benchmark tasks including those drawn from an open-source UAV codebase compare T-SYS with another method of timing-based intrusion detection and assess its effectiveness in terms of detecting attacks as they intrude a system.
This work focuses on the use of deep learning for vulnerability analysis of cyber-physical systems (CPS). Specifically, we considera control architecture widely used in CPS, where the low-level control is based on a feedback controller and an observer (e.g., the extended Kalman filter (EKF)), while also employing an anomaly detector. To facilitate analyzing the impact potential sensing attacks could have on systems with general nonlinear dynamics, we develop learning-enabled attack generators capable of designing stealthy attacks that maximally degrade system operation. We show how such problem can be cast within a learning-based grey-box framework where only parts of the runtime information are known to the attacker. We then introduce two methods for generating effective stealthy attacks, based on feed-forward neural networks (FNN) and recurrent neural networks (RNN). Both types of attack-generator models are trained offline, using a cost function that combines the attack impact on the estimation error (and thus control) and the residual signal used for anomaly detection; this enables the trained models to recursively generate effective yet stealthy sensor attacks in real-time while requiring different levels of system information at runtime. The effectiveness of the proposed methods is demonstrated on several case studies with varying levels of complexity and nonlinearity: inverted pendulum, autonomous driving vehicles (ADV), and unmanned areal vehicles (UAVs).
Many smart home frameworks use applications to automate devices in a smart home. When these applications interact in the same environment, they may cause unintended actions which can lead to a safety violation (e.g., the door is unlocked when the user is not at home). While recent efforts have attempted to address this problem, they do not capture complex app behaviors such as: 1) timed behavior and user inputs (e.g., a lock-door app that locks the door after x duration may cause a door to remain unlocked for a long time if $x$ is set too large.) and 2) interactions between devices and the environment they implicitly affect (e.g., water sprinklers cannot be turned on if the water supply is off). Hence, prior work leads to many false positives and false negatives. In this paper, we present PSA, a practical framework to identify safety intent violations in a smart home. PSA uses parameterized timed automata (PTA) as an expressive abstraction to model smart apps. To parse these apps into PTA, we define mappings from smart app APIs to equivalent PTA primitives. We also provide toolkits to model devices, environments, and their interactions. In designing PSA, we identify and tackle key challenges in ensuring correctness of smart home models and discuss trade-offs between their expressiveness and scalability. We evaluate PSA on 86 apps in the Samsung SmartThings IoT ecosystem. We compare PSA against two state-of-the-art baselines and find: (a) 19 new intent violations and (b) 35% fewer false positives than baselines.