In this paper we formalize in rewriting logic the intended discrete-event semantics of the Lingua Franca coordination language for cyber-physical systems in the simplified setting where each reaction has exactly one trigger. We then show how such Lingua Franca models can be simulated and model checked using Maude, and provide functionality that should make the formal analysis easy to perform also for the Maude non-expert. We illustrate such Maude verification on a number of existing Lingua Franca models, including of a car driver assistance system and of train door controllers. To the best of our knowledge, this is the first verification framework for Lingua Franca that captures the intended semantics of the language, and which therefore provides correct (and state-space efficient) model checking analysis for Lingua Franca.