Spiking Neural Networks (SNNs) offer a biologically inspired approach to modeling neuronal computation, emphasizing timed latency and probabilistic activation over the numerical computations typical of traditional deep-learning models. This paper introduces a modeling framework for SNNs that incorporates the RP-LI&F (Refractory-evolve Probabilistic Leaky Integrate-and-Fire) neuron model to capture realistic neuronal dynamics. We present a prototype, SuNNy, to translate elementary neural bundles and their synaptic connections into formal models compatible with PRISM, enabling model checking of stochastic timing properties using Probabilistic Computation Tree Logic (PCTL). Additionally, our framework integrates with Nengo for simulation, allowing for experimentation on large-scale SNNs. A key challenge addressed is the study of how compound SNN models can meet global reaction requirements based on the stochastic behaviors of individual neural bundles. While the framework supports parametric variations to represent different neuronal states, this work focuses on the core modeling, verification, and simulation techniques. Specific applications, such as simulating impaired neurons, are not explored in this paper but are left for future research. Our approach provides a foundation for both formal verification and simulation of SNNs, bridging the gap between theoretical models and practical tools for analyzing neuronal computations.