García Merayo, María De Las MercedesAndrés Sánchez, CésarNúñez García, ManuelHung, DVKrishnan, P2023-06-202023-06-202009-11978-0-7695-3870-910.1109/SEFM.2009.21https://hdl.handle.net/20.500.14352/453217th IEEE International Conference on Software Engineering and Formal Methods (SEFM 2009). NOV 23-27, 2009. Hanoi, VIETNAMIn this paper we present a formal passive testing framework and use it to analyze time aspects in the Stream Control Transmission Protocol (SCTP). This protocol presents different phases where time aspects are critical. In order to represent temporal requirements we use so-called timed invariants since they allow us to easily verify that the traces collected from the observation of the protocol fulfill the corresponding timed constraints. In addition to introduce our theoretical framework, we report on the results obtained from the application of our techniques over (possibly mutated) traces extracted from runs of the SCTP.engbook parthttp://ieeexplore.ieee.org/stamp/stamp.jsp?tp=&arnumber=5368113http://www.ieee.org/open access519.8Finite-state machinesTimed automataWeak mutationSystemsImplementationSpecificationGenerationComputer ScienceSoftware EngineeringInvestigación operativa (Matemáticas)1207 Investigación Operativa