Business Process Model and Notation (BPMN) is widely used for modelling and communicating workflows, yet it remains qualitative and lacks explicit semantics for timing, probability, and data syn- chronisation. This paper introduces BPMN-T, a timed–probabilistic extension of BPMN endowed with a formal operational semantics. BPMN-T enriches BPMN with temporal, probabilistic, and environ- ment annotations, whose semantics is defined as a Timed–Probabilistic Transition System (TPTS) unifying control-flow, timing, and sto- chastic behaviour. BPMN-T models can be transformed into Timed Automata, Markov Decision Processes, and Probabilistic Timed Au- tomata, thereby enabling comprehensive temporal and probabilistic verification. A verification and synchronisation framework further supports runtime deviation detection and adaptive alignment with real executions, realising verifiable and executable process digital twins.