Petri nets (PNs) are a mathematical and graphical modeling language with powerful analysis techniques. They have been successfully used in several areas, such as business process management, human computer interaction, and pervasive computing. Within these areas, context adaptivity has recently emerged as a new challenge to explicitly address fitness between system behavior and its execution context. However, the existing PN formalisms do not provide reliable modeling, simulation, and verification techniques that can accurately consider the system's execution context and adapt to it in order to reflect the system execution reality. This paper addresses this problem by presenting context-adaptive Petri nets (CAPNs), a formalism that allows the modeling of context-adaptive behavior by integrating the powerful modeling and analysis techniques of PNs with very expressive context data management techniques. The formalism is supported by a tool that allows its modeling, simulation, and verification. The contributions have been validated using a case-based evaluation showing very promising results. CAPNs will allow organizations to accurately describe, enact, and analyze the behavior of their dynamic systems in a more reliable and realistic way, allowing them to leverage more informed decisions, to make better use of their resources, and to increase therefore their competitiveness.